# Search Results

## Cayley's Theorem

The article formalizes the Cayley's theorem saying that every group *G* is isomorphic to a subgroup of the symmetric group on *G*.

## Summary

The paper introduces Cartesian products in categories without uniqueness of **cod **and **dom**. It is proven that set-theoretical product is the product in the category Ens [7].

## Summary

Cayley-Dickson construction produces a sequence of normed algebras over real numbers. Its consequent applications result in complex numbers, quaternions, octonions, etc. In this paper we formalize the construction and prove its basic properties.

## Summary

In this article we prove that fundamental groups based at the unit point of topological groups are commutative [11].

## Summary

In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].

## Arithmetic Operations on Functions from Sets into Functional Sets

In this paper we introduce sets containing number-valued functions. Different arithmetic operations on maps between any set and such functional sets are later defined.

MML identifier: VALUED 2, version: 7.11.01 4.117.1046

## The Correspondence Between n-dimensional Euclidean Space and the Product of n Real Lines

In the article we prove that a family of open *n*-hypercubes is a basis of *n*-dimensional Euclidean space. The equality of the space and the product of *n* real lines has been proven.

## Mazur-Ulam Theorem

The Mazur-Ulam theorem [15] has been formulated as two registrations: cluster bijective isometric -> midpoints-preserving Function of E, F; and cluster isometric midpoints-preserving -> Affine Function of E, F; A proof given by Jussi Väisälä [23] has been formalized.

## Miscellaneous Facts about Open Functions and Continuous Functions

In this article we give definitions of open functions and continuous functions formulated in terms of "balls" of given topological spaces.

## On the Continuity of Some Functions

We prove that basic arithmetic operations preserve continuity of functions.