text:
\begin{document}

\begin{center}
{\Large\bf Tait's Flyping Conjecture \\[1ex]
for 4-Regular Graphs} \\[3ex]
\large J\"org Sawollek\footnote{Fachbereich Mathematik, Universit\"at
Dortmund, 44221 Dortmund, Germany \\ {\em E-mail:\/}
sawollek@math.uni-dortmund.de \\ {\em WWW:\/}
http://www.mathematik.uni-dortmund.de/lsv/sawollek} \\[1ex]
June 22, 1998 (revised: October 9, 2002)
\end{center}
\vspace{4ex}

\begin{abstract}
Tait's flyping conjecture, stating that two reduced, alternating, prime
link diagrams can be connected by a finite sequence of flypes, is
extended to reduced, alternating, prime diagrams of 4-regular graphs in
\sthree . The proof of this version of the flyping conjecture is based
on the fact that the equivalence classes with respect to ambient isotopy
and rigid vertex isotopy of graph embeddings are identical on the class
of diagrams considered. \\[1ex]
{\em Keywords:} Knotted Graph, Alternating Diagram, Flyping Conjecture
\\[1ex]
{\em AMS classification:} 57M25; 57M15
\end{abstract}

\section*{Introduction}
Very early in the history of knot theory attention has been paid to
alternating diagrams of knots and links. At the end of the 19th century
P.G. Tait \cite{tait} stated several famous conjectures on alternating
link diagrams that could not be verified for about a century. The
conjectures concerning minimal crossing numbers of reduced, alternating
link diagrams \cite[Theorems A, B]{mura} have been proved independently
by Thistlethwaite \cite{this}, Murasugi \cite{mura}, and Kauffman
\cite{kauf87}. Tait's flyping conjecture, claiming that two reduced,
alternating, prime diagrams of a given link can be connected by a finite
sequence of so-called {\em flypes\/} (see \cite[page 311]{hkw} for
Tait's original terminology), has been shown by Menasco and
Thistlethwaite \cite{flype}, and for a special case, namely, for
well-connected diagrams, also by Schrijver \cite{schr}.

The present article, as well as \cite{alt}, deals with generalizations
of Tait's conjectures to embeddings of 4-regular (topological) graphs
into 3-space. In \cite{alt} it has been shown that a reduced,
alternating graph diagram $D$ has minimal crossing number. Furthermore,
if $D$ is prime in addition, then a non-alternating diagram that is
equivalent to $D$ cannot have the same crossing number as $D$.

The purpose of this paper is to prove Tait's flyping conjecture for
reduced, alternating, prime diagrams of 4-regular graphs in the 3-sphere
\sthree . The result depends on a suitable definition of primality, see
section \ref{properties}. Its proof is based on the fact that the
equivalence classes with respect to rigid vertex isotopy and ambient
isotopy of graph diagrams are identical on the class of diagrams under
consideration.

Definitions of these two equivalence relations for graph diagrams are
given in section \ref{diagrams}. Then, in section \ref{tangleinv}, the
notion of {\em tangles\/} is introduced to derive invariants of graph
diagrams and to give, via transformation tangles, a description of a
sequence of Reidemeister V moves (see Fig. \ref{reidemeister}) applied
to a graph vertex. In section \ref{properties} certain properties of
graph diagrams are discussed, and two important theorems on reduced,
alternating diagrams are stated. After, in section \ref{mainsec}, Tait's
flyping conjecture has been shown to be an immediate consequence of the
fact that the two equivalence classes mentioned above coincide for
reduced, alternating, prime graph diagrams, the latter statement is
finally proved in section \ref{mainproof}.

\section{Diagrams of 4-Regular Graphs}
\label{diagrams}

Embedding graphs into \sthree\ extends, in a natural way, the classical
knot theoretical problem of embedding one or more disjoint copies of the
1-sphere $\mathbb S^1$ into \sthree\ where the resulting images are
called {\em knots\/} and {\em links}, respectively. Classical
terminology of knot theory can be found in \cite{bur} or \cite{rol}, see
\cite{kaufbook}, \cite{kawa}, \cite{lick}, \cite{mubook} for more recent
introductions to the field.

A {\em topological graph\/} is a 1-dimensional cell complex which is
related to an abstract graph in the obvious way. In the following,
always $4$-regular graphs, which are allowed to have multiple edges or
loops, are considered. Vertices of degree two may occur but are
neglected since they are uninteresting for a topological treatment.

If $G$ is a topological graph, then a {\em graph $\mathcal G$ in
\sthree} is the image of an embedding of $G$ into \sthree. Two graphs
${\mathcal G}_1$, ${\mathcal G}_2$ in \sthree\ are called {\em
equivalent with respect to ambient isotopy\/} or {\em ambient
isotopic\/} if there exists an orientation preserving autohomeomorphism
of \sthree\ which maps ${\mathcal G}_1$ onto ${\mathcal G}_2$.
Embeddings of topological graphs in \sthree\ can be examined via {\em
regular graph diagrams}, i.e., images under regular projections to an
appropriate sphere equipped with over-under information at double
points. Two graph diagrams $D$ and $D'$ are called {\em equivalent with
respect to ambient isotopy\/} or {\em ambient isotopic\/} if one can be
transformed into the other by a finite sequence of Reidemeister moves
I--V (see Fig. \ref{reidemeister}) combined with orientation preserving
homeomorphisms of the sphere to itself.
\begin{figure}[htb]
\begin{tabular}{rccccccc}
I) & {\knot a} & $\longleftrightarrow$ & {\knot b} &
$\longleftrightarrow$ & {\knot c} \\[2ex]
II) & {\knot d} & $\longleftrightarrow$ & {\knot e \hspace{0.5cm} f}
\\[2ex]
III) & {\knot g} & $\longleftrightarrow$ & {\knot h} & , & {\knot i} &
$\longleftrightarrow$ & {\knot j} \\[2ex]
IV) & {\knot k} & $\longleftrightarrow$ & {\knot l} & , & {\knot m} &
$\longleftrightarrow$ & {\knot n} \\[2ex]
V) & {\knot o} & $\longleftrightarrow$ & {\knot p} &
$\longleftrightarrow$ & {\knot q} \\[2ex]
VI) & {\knot r} & $\longleftrightarrow$ & {\knot p}
\end{tabular}
\vspace{2ex}

\caption{Reidemeister moves}
\label{reidemeister}
\end{figure}
Two graphs in \sthree\ are ambient isotopic if and only if they have
diagrams that are ambient isotopic (see \cite{kauf89} or \cite{yet}).

Soon after the discovery of polynomial link invariants which fulfil
certain recurrence formulas, such as the Jones polynomial and its
generalizations, it had been tried to extend these invariants to graphs
in 3-space. Only quite recently such an invariant for arbitrary
topological graphs has been found by Yokota \cite{yoko} (see \cite{alt}
for a different approach in the case of 4-regular graphs). Yokota's
invariant manages the difficulty to be invariant under Reidemeister move
V which before had been the main obstacle for a full generalization of
combinatorial link invariants to knotted graphs.

Besides ambient isotopy there is a further equivalence relation for
graph diagrams which avoids Reidemeister move V and which will be
important for the purposes of this paper: two graph diagrams $D$ and
$D'$ are called {\em equivalent with respect to rigid vertex isotopy\/}
or {\em rigid vertex isotopic\/} if one can be transformed into the
other by a finite sequence of Reidemeister moves I--IV and VI (see Fig.
\ref{reidemeister}) combined with orientation preserving homeomorphisms
of the sphere to itself. Rigid vertex isotopy corresponds to an
equivalence relation on graphs in \sthree\ where a small neighbourhood
of each graph vertex is contained inside a disk, and only those
orientation preserving autohomeomorphisms of \sthree\ are considered
that respect these disks (see \cite{jomi}, \cite{kauf89}, \cite{yama}).
Observe that Reidemeister moves I--V imply Reidemeister move VI, thus
rigid vertex isotopic graph diagrams are ambient isotopic. See Fig.
\ref{counter} for two ambient isotopic diagrams which are not rigid
vertex isotopic.

For the sake of shortness, the phrase {\em graph diagram\/} will always
mean {\em (regular) diagram of a 4-regular graph in \sthree\/} in the
subsequent text, and throughout the article a {\em link\/} will be
considered as 4-regular graph in \sthree\ without vertices of degree
four. Of course, the equivalence classes with respect to rigid vertex
isotopy and ambient isotopy coincide for links.

\section{Tangles, and Invariants of Graph Diagrams}
\label{tangleinv}

In this section, the notion {\em rational tangle\/} is introduced for
two purposes: to define invariants of graph diagrams with respect to
ambient isotopy, and to describe the effect of a sequence of
Reidemeister moves applied to a graph vertex. The definitions and
notations used here are due to Conway \cite{con}.

A {\em tangle\/} is a part of a link diagram in form of a disk with four
arcs emerging from it, see Fig. \ref{tangle} (left),
\begin{figure}[htb]
\begin{picture}(12,2.5)
\thicklines
\put(0.5,0.8){\knot S}
\put(1.2,1.1){\line(0,1){0.45}}
\put(1.2,1.1){\line(1,0){0.25}}
\put(0.4,2){$a$}
\put(2.1,2){$b$}
\put(2.1,0.4){$c$}
\put(0.4,0.4){$d$}
\put(4.6,0.8){\knot T}
\put(5.3,1.1){\line(0,1){0.45}}
\put(5.3,1.1){\line(1,0){0.25}}
\put(7.45,1.1){\line(0,1){0.45}}
\put(7.45,1.1){\line(1,0){0.25}}
\put(5.3,2.1){$s$}
\put(7.5,2.1){$t$}
\put(6.1,0){$s+t$}
\put(8.9,0.8){\knot T}
\put(9.95,1.45){\line(-1,0){0.45}}
\put(9.95,1.45){\line(0,-1){0.25}}
\put(11.75,1.1){\line(0,1){0.45}}
\put(11.75,1.1){\line(1,0){0.25}}
\put(9.6,2.1){$s$}
\put(11.8,2.1){$t$}
\put(10,0){$s \cdot t = s t$}
\end{picture}
\caption{\label{tangle} A tangle, and tangle operations}
\vspace{1ex}

\end{figure}
where the tangle's position is indicated by an L-shaped symbol and its
emerging arcs are labeled with letters $a$, $b$, $c$, $d$ in a clockwise
ordering (or simply one of them with "$a$"). Two tangles are said to be
{\em equivalent (with respect to ambient isotopy)\/} if one can be
transformed into the other by a finite sequence of Reidemeister moves of
type I--III and autohomeomorphisms of the disk which keep the boundary
fixed. In the following, a notational difference between a tangle and
the corresponding equivalence class will be avoided. Some basic tangles
are $0 = \raisebox{2pt}{\knot V}$, $\infty = \raisebox{2pt}{\knot W}$,
$1 = \mbox{\knot J}$, $\overline{1} = -1 = \mbox{\knot U}$.

For tangles $s$ and $t$, the operations + and $\cdot$ are defined as
depicted in Fig. \ref{tangle}. The tangles $0$, $n = 1 + \ldots + 1$,
and $\overline{n} = \overline{1} + \ldots + \overline{1}$ are called
{\em integer tangles}. If a tangle $t$ is of the form $t = a_1 \ldots
a_n$ with integer tangles $a_1, \ldots , a_n$ or if $t = \infty$, then
$t$ is called {\em rational tangle}. Let $\cal K$ denote the set of all
(equivalence classes of) rational tangles.

For a rational tangle $a_1 \ldots a_n$ the evaluation of the continued
fraction
\[ a_n + \frac{1}{a_{n-1} + \ldots + \frac{\textstyle 1}{\textstyle a_2 +
\frac{\textstyle 1}{\textstyle a_1}}} \]
gives a number in $\mathbb Q \cup \{ \infty \}$ where the obvious rules
for handling "$\infty$", such as $\frac{1}{\infty} = 0$, are applied, if
necessary, during the calculation. It is known that two rational tangles
are equivalent if and only if the values of the corresponding continued
fractions are identical (see \cite{con}, \cite{bur} for classical
proofs, and \cite{gold} for an elementary combinatorial proof).
Therefore, a rational tangle $r$ can be identified with this number,
thus let $r$ denote an element of $\cal K$ as well as the corresponding
value in $\mathbb Q \cup \{ \infty \}$, and let $|r|$ denote the
tangle's {\em crossing number}, i.e., the minimal number of crossings in
any diagram belonging to the equivalence class represented by $r$.
Furthermore, a rational tangle contained in ${\mathcal K} \setminus \{
0, \infty, 1, \overline{1} \}$ can be expressed in a uniquely determined
{\em normal form\/} $a_1 \ldots a_n$ such that $|a_1| \geq 2$, $a_2 \neq
0$, \ldots , $a_{n-1} \neq 0$, and all $a_i \geq 0$ or all $a_i \leq 0$.
The normal forms of the remaining four tangles are the obvious ones.
Tangles in normal form have minimal number of crossings.

From a given graph diagram $D$ there can be obtained link diagrams by
substituting rational tangles for the graph vertices (see
\cite{four-reg}). To do this in a well-defined way, it is necessary
to give an ordering to the $k \geq 0$ graph vertices, i.e., a bijection
from the set $\{ 1 , \ldots , k \}$ to the set of graph vertices
contained in $D$ called {\em vertex-enumeration}, and an {\em
orientation\/} to each vertex, i.e., labeling an edge incident to the
vertex with the letter $a$. In the following, mainly the rational
tangles $0$, $\infty$, and $1$ will be needed. Substituting $0$ or
$\infty$ for graph vertices is done as depicted in Fig. \ref{replace},
\begin{figure}[htb]
\begin{picture}(13.5,4.5)
\thinlines
\put(0.5,2){$D$}
\put(1.5,0.8){\knot X}
\put(3.6,3.5){$a$}
\put(4.2,3.05){2}
\put(2.5,1.1){$a$}
\put(2.75,0.2){1}
\put(6,2.1){\vector(1,0){1}}
\put(8.5,0.8){\knot Y}
\put(12.5,2){$D_{0, \infty}$}
\end{picture}
\caption{Cutting open vertices}
\label{replace}
\end{figure}
that is to say, vertices are cut open in one of the two possible ways
determined by the vertex-orientation. Substituting the tangle $1$
corresponds to replacing a graph vertex with a crossing {\knot J} with
respect to the vertex-orientation given.

Replacing vertices of a graph diagram with all rational tangles, or, to
be precise, with a representative of each equivalence class (e.g., all
rational tangles in normal form),  gives an invariant of diagrams with
respect to ambient isotopy that consists of infinitely many link
diagrams (see \cite{four-reg}).

Getting invariants with respect to rigid vertex isotopy is much easier:
just substiute one or more arbitrary (but fixed) tangles for each vertex
and get rid of the ambiguity arising from different vertex-orientations
by considering all choices of such orientations. It is readily checked
that this gives well-defined invariants of graph diagrams under
Reidemeister moves I--IV and VI. For example, the unordered tuple
$(D_{0,0}, D_{0, \infty}, D_{\infty, 0}, D_{\infty, \infty})$ defines a
rigid vertex invariant of the graph belonging to the diagram $D$
depicted in Fig. \ref{replace}. Observe that the invariant $C(G)$
defined in \cite{kauf89} and denoted by ${\cal C}(G)$ in \cite{kauvo} is
a special version of this type of invariants, induced by the tangles $0$
and $1$, where sets are used instead of -- more informative -- unordered
tuples.

Another point of view in considering ambient isotopic graph diagrams is
to observe that the Reidemeister moves of type V, applied to a vertex
during a transformation of one graph diagram into another, can be
collected to a rational tangle. For example, the transformation depicted
in Fig. \ref{sequence}
\begin{figure}[htb]
\begin{picture}(12,2.5)
\thicklines
\put(3.5,1.3){\knot p}
\put(3.2,2.1){$a$}
\put(6.3,1.4){\vector(1,0){1}}
\put(8.7,2.1){$a$}
\put(9,1.5){\knot F}
\end{picture}
\caption{Applying a sequence of Reidemeister V moves}
\label{sequence}
\end{figure}
can be described by the tangle $t = 2 \, 1 \, 0 \in {\mathcal K}$.

\begin{dfn}
Let $D$, $D'$ be ambient isotopic graph diagrams with $k \geq 1$
vertices and given vertex-enumerations and -orientations. If $D_{0,
\ldots , 0} = D'_{t_1, \ldots , t_k}$ with tangles $t_1, \ldots, t_k$
then $t_j$, for $j \in \{ 1, \ldots , k \}$, is called {\em $j$--th
transformation tangle\/} of the transformation from $D$ into $D'$. If
$r_1, \ldots , r_k$ are rational tangles then let $r_j * t_j$ denote the
tangle into which $r_j$ is transformed when replacing the $j$--th vertex
of $D$ with $r_j$, that is to say, $D_{r_1, \ldots , r_k} = D'_{r_1 *
t_1, \ldots , r_k * t_k}$.
\end{dfn}

Considering Reidemeister move VI, it may be assumed, without loss of
generality, that only the {\em admissible\/} Reidemeister moves of type
V depicted in Fig. \ref{admissible} have to be applied during a
transformation.
\begin{figure}[htb]
\begin{picture}(12,4.5)
\put(2.8,2.5){\begin{tabular}{cccccccc}
{\knot o} & $\longleftrightarrow$ & {\knot p} & $\longleftrightarrow$
& {\knot q} \\[2ex]
{\knot Q} & $\longleftrightarrow$ & {\knot p} & $\longleftrightarrow$ &
{\knot R}
\end{tabular}}
\put(5.9,4){$a$}
\put(2.7,4){$a$}
\put(8.6,4){$a$}
\put(5.9,1.85){$a$}
\put(3,1.85){$a$}
\put(8.8,1.85){$a$}
\end{picture}
\caption{Admissible Reidemeister moves of type V}
\label{admissible}
\end{figure}
Furthermore, if the orientation of a vertex is chosen appropriately, the
corresponding transformation tangle $t$ can be written as $t = b_1
\ldots b_s \neq \infty$ with integer tangles $b_1, \ldots , b_s$ such
that $b_1 \ldots b_s$ is in normal form. A rational tangle $r = a_1
\ldots a_l$ is transformed by the transformation tangle $t$ into the
tangle  $r*t = a_1 \ldots a_{l-1} (a_l+b_1) b_2 \ldots b_s$. Especially,
the tangles $0$ and $\infty $ are transformed into $t$ and into a tangle
equivalent to $b_2 \ldots b_s$, respectively, see Fig.
\ref{trivialreplacement}.
\begin{figure}[htb]
\begin{picture}(12,2)
\thicklines
\put(0.5,1.4){\knot C}
\put(2,1.5){\vector(1,0){1}}
\put(3.5,1.5){\knot K}
\put(7.5,1.4){\knot B}
\put(9,1.5){\vector(1,0){1}}
\put(10.5,1.5){\knot L}
\end{picture}
\caption{Replacing a graph vertex with 0 and $\infty$}
\label{trivialreplacement}
\end{figure}

\begin{rem}
It is not difficult to see that the inverse of a transformation
described by a tangle $t = b_1 \ldots b_s$ is given by
$t' = \overline{b_s \ldots b_1}$, i.e., if $D_0 = D'_t$ then $D'_0 =
D_{t'}$ for ambient isotopic graph diagrams $D$ and $D'$ in which
corresponding vertices have been replaced.
\end{rem}

\section{Properties of Graph Diagrams}
\label{properties}

A link diagram is said to be {\em alternating\/} if over- and
undercrossings are alternating with each other while walking along any
link component in the diagram. A link diagram $D$ is called {\em
reduced\/} if it contains no {\em isthmus}, i.e., a crossing $p$ such
that $D \setminus \{ p \}$ has more components than $D$. A connected
link diagram is said to be {\em prime\/} if it cannot be written as
connected sum of two link diagrams both of which having at least one
crossing.

\begin{dfn}
A graph diagram $D$ is said to be {\em alternating/reduced/prime\/} if,
corresponding to an arbitrarily chosen vertex-enumeration and
-orientation, the link diagrams $D_{i_1, \ldots , i_k}$ are
alternating/reduced/prime for every choice of $i_1, \ldots , i_k \in \{
0, \infty \}$.
\end{dfn}

An example of a graph diagram that is alternating, reduced, and prime is
depicted in Fig. \ref{replace}.

\begin{rem}
\begin{enumerate}
\item The definition of primality for graph diagrams does not seem to be
the natural one, but it is the one that fits into the context (see the
counterexample contained in the remark at the end of this section).
\item In contrast to the case of link diagrams, a graph diagram that is
not reduced may be {\em irreducible}, i.e., the number of the diagram's
crossings is minimal. See \cite{alt} for examples.
\item A prime graph diagram which has more than one crossing is reduced.
\item The definition of "alternating" for graph diagrams has been
adapted to the definitions of "prime" and "reduced". Of course, a graph
diagram $D$ is alternating if and only if there is a choice of
vertex-orientations such that $D_{1, \ldots , 1}$ is alternating.
\end{enumerate}
\end{rem}

It is remarkable that, after introducing an appropriate definition of
primality (see \cite{alt}), for a 4-regular graph in \sthree\ which
possesses a reduced, alternating diagram the property to be prime can be
deduced from the corresponding property of its diagram. A proof of this
fact for link diagrams is due to Menasco \cite{mena}, and it can easily
be extended to 4-regular graphs in \sthree, see \cite[Theorem 8]{alt}.
The following statement is an immediate consequence.

\begin{thm}
\label{graphmenasco}
Let $D$ and $D'$ be ambient isotopic graph diagrams that are alternating
and reduced. Then:
\begin{enumthm}
\item $D$ is connected if and only if $D'$ is connected.
\item $D$ is prime if and only if $D'$ is prime.
\end{enumthm}
\end{thm}
\qed

To prove Tait's flyping conjecture for graph diagrams, a generalization
of a Tait conjecture concerning minimal crossing numbers, cited in the
introduction, will be needed. A proof can be found in \cite[Theorem
9]{alt}.

\begin{thm}
\label{altmin}
Let $\mathcal G$ be a 4-regular graph in \sthree, and let $D$ be a
reduced, alternating, prime diagram of $\mathcal G$ with $n$ crossings.
Then there is no diagram of $\mathcal G$ having less than $n$ crossings,
and any non-alternating diagram of $\mathcal G$ has more than $n$
crossings.
\end{thm}
\qed

\section{Tait's Flyping Conjecture}
\label{mainsec}

The definition of a tangle as part of a link diagram can be extended to
graph diagrams in the obvious way, and appropriate equivalence relations
can be introduced likewise. In the following, always those generalized
tangles are considered.

\begin{dfn}
A {\em flype\/} is a local change in a graph diagram as depicted in Fig.
\ref{flype}.
\begin{figure}[htb]
\begin{picture}(13,2)
\thicklines
\put(2.3,0.5){\knot O}
\put(4.2,0.8){\line(0,1){0.45}}
\put(4.2,0.8){\line(1,0){0.25}}
\put(4.2,0){$t$}
\put(6.5,0.9){$\longleftrightarrow$}
\put(9,0.5){\knot P}
\put(9.4,0.8){\line(0,1){0.1}}
\put(9.4,0.95){\line(0,1){0.1}}
\put(9.4,1.1){\line(0,1){0.1}}
\put(9.4,1.25){\line(1,0){0.1}}
\put(9.55,1.25){\line(1,0){0.1}}
\put(9.4,0){$t_h$}
\end{picture}
\caption{A flype}
\label{flype}
\end{figure}
Using Conway's notation \cite{con}, this corresponds to a transformation
of the form $1 + t \leftrightarrow t_h + 1$ or $\overline{1} + t
\leftrightarrow t_h + \overline{1}$.
\end{dfn}

In \cite{flype} Tait's flyping conjecture is proved for diagrams of
4-regular rigid vertex graphs to obtain the validity of Tait's original
conjecture. This result is stated in the following theorem where, as
well as in the subsequent text, the phrase {\em sequence of flypes\/} is
an abbreviation for {\em sequence of flypes plus orientation preserving
autohomeomorphisms of the sphere}. It should be mentioned that the
notion of primality for graph diagrams used in \cite{flype} is different
from the one used in the present text. Indeed, a graph diagram that is
prime with respect to the definition given above is prime in the sense
of \cite{flype}, too, and thus the result from \cite{flype} can be
adopted here.

\begin{thm}
\label{rigidflype}
Let $D$ and $D'$ be rigid vertex isotopic graph diagrams that are
reduced, alternating, and prime. Then there exists a finite sequence of
flypes which transforms $D$ into $D'$.
\end{thm}
\qed

Considering ambient isotopy of graph diagrams, the desired extension of
Tait's flyping conjecture to 4-regular graphs can be deduced immediately
from the next theorem. The proof of the theorem will be given in section
\ref{mainproof}.

\begin{thm}
\label{main}
Let $D$ and $D'$ be graph diagrams that are reduced, alternating, and
prime. Then $D$ and $D'$ are equivalent with respect to ambient isotopy
if and only if they are equivalent with respect to rigid vertex isotopy.
\end{thm}
\medskip

\begin{cor}
\label{maincor}
Let $D$ and $D'$ be ambient isotopic graph diagrams that are reduced,
alternating, and prime. Then there exists a finite sequence of flypes
which transforms $D$ into $D'$.
\end{cor}
\qed

\begin{rem}
Theorem \ref{main} does not hold in general without assuming primality.
A counterexample is depicted in Fig. \ref{counter}: the two (alternating
and reduced) graph diagrams obviously are equivalent with respect to
ambient isotopy, but they are not rigid vertex isotopic because cutting
open vertices in the two possible ways gives diagrams of 2- and
3-component links, respectively, where the diagrams belonging to the
3-component link are equivalent, and the diagrams belonging to the
2-component link correspond to different mirror images of a chiral link.
\begin{figure}[htb]
\begin{picture}(13,3.5)
\put(1.5,0){\knot H}
\put(6.5,1.5){$\longleftrightarrow$}
\put(8.5,0){\knot I}
\end{picture}
\caption{Ambient isotopic diagrams that are not rigid vertex isotopic}
\label{counter}
\end{figure}
\end{rem}

\section{Proof of Theorem \ref{main}}
\label{mainproof}

Theorem \ref{main} is proved by induction on the number of graph
vertices. The main ingredient for the induction step comes from the fact
that transformation tangles which describe a transformation between
reduced, alternating, prime diagrams always are trivial, and thus
replacing a vertex in both diagrams with the same tangle, for
corresponding vertices and with respect to appropriately chosen
vertex-orientations, gives ambient isotopic graph diagrams with one
vertex less. As a main tool for showing this claim, properties of the
{\em Kauffman polynomial\/} \cite{kauf90} of link diagrams and its
relations to a diagram's crossing number are used.

\begin{dfn}
The {\em Kauffman polynomial\/} $\Gamma_D(a,z) \in \mathbb Z [a^{\pm 1},
z^{\pm 1}]$ of a link diagram $D$ is defined by the following
properties.
\begin{enumdfn}
\item $\Gamma_D(a,z)=1$ if $D$ is a simple closed curve
\item $\Gamma_{D_{\mbox{\knot s v}}} = a \Gamma_{D_{\mbox{\knot u}}}$
and $\Gamma_{D_{\mbox{\knot t v}}} = a^{-1} \Gamma_{D_{\mbox{\knot u}}}$
\item $\Gamma_{D_{\mbox{\knot s}}} + \Gamma_{D_{\mbox{\knot t}}} \; = \;
z ( \Gamma_{D_{\mbox{\knot w}}} + \Gamma_{D_{\mbox{\knot x}}})$
\end{enumdfn}
The highest exponent in the variable $z$ is called {\em z-degree\/} of
$\Gamma_D$.
\end{dfn}

In the following, an {\em $n$-bridge\/} $b$ in a link diagram $D$ is an
arc of $D$ that contains only overcrossings or only undercrossings, and
the number of these crossings is $n$, the {\em length\/} of $b$.

The $z$-degree of the Kauffman polynomial heavily depends on the length
of the longest bridge contained in a diagram. A precise formulation of
this fact is given in the next theorem, for a proof see \cite[Theorems
4, 5]{this}.

\begin{thm}
\label{elementary}
Let $D$ be a link diagram with $n \geq 1$ crossings, and let $b \geq 1$
be the length of an arbitrary bridge contained in $D$. Then:
\begin{enumthm}
\item $\zdeg{D} \leq n - b \leq n - 1$
\item $\zdeg{D} = n - 1$ if and only if $D$ is reduced, alternating,
prime
\end{enumthm}
\end{thm}
\qed

Now two technical lemmas on Kauffman polynomials are stated which are
needed to deduce the crucial Lemma \ref{transform}. For a proof of the
first lemma see \cite[Lemmas 8, 10]{four-reg}.

\begin{lemma}
\label{tanglesum}
Let $D$ be a reduced, alternating, prime graph diagram with \mbox{$k
\geq 1$} vertices and $n$ crossings, and let $r$ be a rational tangle in
normal form. Furthermore, let $i_1, \ldots, i_{k-1} \in \{ 0, \infty
\}$. Then, corresponding to an arbitrarily chosen vertex-enumeration and
-orientation, the following holds for the link diagram $D' = D_{i_1,
\ldots, i_j, r, i_{j+1}, \ldots, i_{k-1}}$ with $j \in \{ 1, \ldots, k
\}$.
\[ \zdeg{D'} \; = \; \left\{
\begin{array}{ll}
n + |r| - 1 & \mbox{if $D'$ is alternating} \\[1ex]
n + |r| - 2 & \mbox{if $D'$ is not alternating and } |r| \neq 1
\end{array} \right. \]
\end{lemma}
\qed

\begin{dfn}
Let $D$ be an alternating graph diagram with $k \geq 1$ vertices and $n$
crossings, supplied with an arbitrarily chosen vertex-enumeration and a
vertex-orientation such that $D_{\overline{1}, \ldots, \overline{1}}$ is
alternating. Then $D$ is called {\em degree-reducing\/} if
$\zdeg{D_{\varepsilon_1, \ldots, \varepsilon_k}} \leq n-2$ for every
choice of $\varepsilon_1, \ldots, \varepsilon_k \in \{ 0, \infty, 1 \}$
with $\varepsilon_j = 1$ for at least one index $j \in \{ 1, \ldots, k
\}$.
\end{dfn}

\begin{lemma}
\label{ratins}
Let $D$ be a reduced, alternating, prime, degree-reducing graph diagram
with $k \geq 1$ vertices and $n$ crossings, supplied with an arbitrarily
chosen vertex-enumeration and a vertex-orientation such that
$D_{\overline{1}, \ldots, \overline{1}}$ is alternating. If $r_1, \ldots
r_k$ are rational tangles in normal form having at least two crossings
each, then
\[ \zdeg{D_{r_1, \ldots, r_k}} \; = \; n + |r_1| + \ldots + |r_k| - t_+
- 1 \]
holds, where $t_+$ denotes the number of indices $j$ with $r_j > 0$.
\end{lemma}

\begin{proof} As a consequence of Lemma \ref{tanglesum}, replacing a
vertex of $D$ with a negative tangle $r$ yields a graph diagram
$D'$ with $k-1$ vertices and $n + |r|$ crossings that is reduced,
alternating, prime ($\zdeg{D'_{\varepsilon_1, \ldots,
\varepsilon_{k-1}}} = n + |r| - 1$ with $\varepsilon_i \in \{ 0,
\infty\}$ can only be fulfilled if $D'$ possesses all three properties).
Thus it may be assumed that $t_+ = k$. In the following, it is shown
that
\[ \zdeg{D_{r_1, \ldots, r_k}} \left\{
\begin{array}{ll}
= n + |r_1| + \ldots + |r_k| - k - 1 & \mbox{if $r_j \neq 1$ for all
$j$} \\[1ex]
\leq n + |r_1| + \ldots + |r_k| - k - 2 & \mbox{otherwise}
\end{array} \right. \]
holds for positive rational tangles $r_1, \ldots, r_k$ having at least
one crossing each. Since Lemma \ref{tanglesum} and Theorem
\ref{elementary} (if $r_k = 1$) immediately give the result for the case
$k=1$, let $k \geq 2$ for the rest of the proof.

Let $l$ denote the number of indices $j$ with $r_j=1$. The proof is done
by induction on $k-l \geq 0$. If $k-l = 0$ then $r_1 = \ldots = r_k =
1$, and therefore $\zdeg{D_{r_1, \ldots, r_k}} \leq n-2$ since $D$ is
degree-reducing. Thus let $k-l \geq 1$. Then $r_j \neq 1$ for at least
one index $j \in \{ 1, \ldots , k \}$, and without loss of generality
let $r_k = a_1 \ldots a_s \neq 1$.

At first consider the case that $r_k = 2$. Then the recurrence formula
for the Kauffman polynomial gives:
\[ \Gamma_{D_{r_1, \ldots , r_{k-1}, 2}} \, = \, \Gamma_{D_{r_1, \ldots ,
r_{k-1}, 0}} + z(a \Gamma_{D_{r_1, \ldots , r_{k-1}, \infty}} +
\Gamma_{D_{r_1, \ldots , r_{k-1}, 1}}) \]
Applying the induction hypothesis immediately yields the desired
inequality if $l \geq 1$ and the desired equality if $l=0$.

If $r_k = a_1$ is integral then the claimed result can be verified
inductively by considering the corresponding recurrence formula, and a
further induction on $s$ completes the proof.
\qed
\end{proof}

An important class of degree-reducing diagrams is defined next.

\begin{dfn}
An alternating graph diagram $D$ with $k \geq 1$ vertices is called {\em
vertex-separating\/} if there exist disjoint tangles $t_1, \ldots, t_k$
in $D$ such that each tangle $t_i$ contains exactly one graph vertex and
replacing this vertex with a crossing {\knot J}, corresponding to an
appropriately chosen vertex-orientation, yields a 3-bridge inside $t_i$.
\end{dfn}

An example of an alternating graph diagram that is vertex-separating is
depicted in Fig. \ref{vertexsep}.
\begin{figure}[htb]
\begin{picture}(12,11.5)
\put(5.3,0.5){\knot M}
\put(5.3,0.5){\knot N}
\end{picture}
\caption{A reduced, alternating, prime, vertex-separating graph diagram}
\label{vertexsep}
\end{figure}

\begin{lemma}
A vertex-separating graph diagram is degree-reducing.
\end{lemma}

\begin{proof} Considering the {\em numerator formula for the Kauffman
polynomial\/} that has been deduced in \cite{four-reg}, p. 733, it can
easily be shown via induction on $l$ that
\[ \zdeg{D_{\varepsilon_1, \ldots, \varepsilon_k}} \; \leq \; n - l - 1
\; \leq \; n - 2 \]
holds for a vertex-separating graph diagram $D$ with $k$ vertices and
$n$ crossings where $\varepsilon_1, \ldots, \varepsilon_k \in \{ 0,
\infty, 1 \}$ have been replaced for the vertices and $l \geq 1$ denotes
the number of indices $j$ with $\varepsilon_j = 1$.
\qed
\end{proof}

\begin{lemma}
\label{transform}
Let $D$ and $D'$ be ambient isotopic graph diagrams with $k \geq 1$
vertices, and let $t_1, \ldots, t_k$ denote the transformation tangles
belonging to a sequence of Reidemeister moves which realizes the
equivalence between $D$ and $D'$, corresponding to chosen
vertex-enumerations and -orientations of the diagrams. If $D$ and $D'$
both are reduced, alternating, and prime then $|t_1| = \ldots = |t_k| =
0$.
\end{lemma}

\begin{proof} Obviously, a prime, reduced graph diagram with $k \geq 1$
vertices has at least two crossings, and, applying Theorem \ref{altmin},
it is clear that $D$ and $D'$ have identical crossing number $n \geq 2$.
Without loss of generality, let vertex-enumerations be chosen such that
the $j$-th vertex of $D$ is mapped to the $j$-th vertex of $D'$ when the
sequence of Reidemeister moves which transforms $D$ into $D'$ is
applied. For the sake of notational convenience, assume that
$D_{\overline{1}, \ldots, \overline{1}}$ and $D'_{\overline{1}, \ldots,
\overline{1}}$ are alternating.

Suppose that some of the transformation tangles, which may assumed to be
in normal form, have more than one crossing. Define $\varepsilon_i :=
\infty$ if $|t_i| = 1$ and $\varepsilon_i := 0$ if $|t_i| \neq 1$. Then
on the one hand, $\zdeg{D_{\varepsilon_1, \ldots, \varepsilon_k}} = n-1$
since $D$ is reduced, alternating, prime. On the other hand,
$\zdeg{D'_{\varepsilon_1*t_1, \ldots, \varepsilon_k*t_k}} \geq n$, by
Lemma \ref{ratins}, since $\varepsilon_i*t_i = \infty$ if $|t_i| = 1$
(perform a Reidemeister move I) and $D'_{\varepsilon_1*t_1, \ldots,
\varepsilon_k*t_k}$ can be thought to arise from a vertex-separating
graph diagram, namely, the diagram in which the vertices $v_i$ with
$|t_i| \neq 1$ not have been replaced (if there is no 3-bridge after
replacing one of these vertices by a crossing then perform a flype
as depicted in Fig. \ref{vertexflype}).
\begin{figure}[htb]
\[ \mbox{\knot 1} \qquad \longrightarrow \qquad \mbox{\knot 2} \]
\caption{Flyping a vertex}
\label{vertexflype}
\end{figure}
This gives a contradiction
because $D_{\varepsilon_1, \ldots, \varepsilon_k} =
D'_{\varepsilon_1*t_1, \ldots, \varepsilon_k*t_k}$. Thus $|t_i| \leq 1$
for all indices $i$.

Now suppose there is an index $j$ with $|t_j| = 1$. Define
$\varepsilon_j := 0$ and $\varepsilon_i := \infty$ for $i \neq j$. Then
$\zdeg{D_{\varepsilon_1, \ldots, \varepsilon_k}} = n-1$ as in the
previous case, but it is $\varepsilon_i * t_i = \infty$ for $i \neq j$
and therefore either $\zdeg{D'_{\varepsilon_1*t_1, \ldots,
\varepsilon_k*t_k}} \leq n-2$ if $t_j = 1$ because the diagram contains
a 3-bridge (otherwise there would be a contradiction to reducedness and
primality of the diagram), or $\zdeg{D'_{\varepsilon_1*t_1, \ldots,
\varepsilon_k*t_k}} = n$ if $t_j = \overline{1}$ because the diagram is
reduced, alternating, and prime. Again a contradiction in both cases,
thus $|t_i| = 0$ for all indices $i$.
\qed
\end{proof}

Lemma \ref{transform} shows that transformation tangles belonging to two
ambient isotopic graph diagrams always are trivial if both diagrams are
reduced, alternating, and prime. Thus replacing vertices of such
diagrams with tangles gives an ambient isotopy invariant of graph
diagrams up to a choice of vertex-orientations.
Especially:

\begin{cor}
\label{trafocor}
Let $D$ and $D'$ be ambient isotopic graph diagrams with $k \geq 1$
vertices that are reduced, alternating, and prime. Let $D_1$, $D'_1$
denote diagrams that arise from substituting the tangle $1$ for
corresponding vertices of $D$ and $D'$, respectively, and let
vertex-orientations be chosen such that $D_1$ and $D_1'$ both are
alternating. Then $D_1$ and $D'_1$ are equivalent with respect to
ambient isotopy.
\qed
\end{cor}

\begin{rem}
Observe that it is not clear, at this stage, that the diagrams $D_1$ and
$D'_1$ of Corollary \ref{trafocor} are rigid vertex isotopic since the
sequence of Reidemeister moves of type V applied to a vertex leads to a
transformation tangle which is equivalent to a trivial tangle but not
necessarily equal to it.
\end{rem}

\begin{lemma}
\label{rot}
The graph diagrams that are depicted in Fig. \ref{rotate}
\begin{figure}[htb]
\begin{picture}(8,2)
\thicklines
\put(1.8,0.5){\knot G}
\put(4.85,0.8){\line(0,1){0.45}}
\put(4.85,0.8){\line(1,0){0.25}}
\put(6.5,0.9){$\longleftrightarrow$}
\put(8,0.5){\knot G}
\put(11.4,1.15){\line(0,-1){0.25}}
\put(10.95,0.9){\line(1,0){0.45}}
\end{picture}
\caption{Rigid vertex isotopic diagrams}
\label{rotate}
\end{figure}
are rigid vertex isotopic.
\end{lemma}

\begin{proof}
Perform the transformations depicted in Fig. \ref{picproof},
where "R." is an abbreviation for "Reidemeister", and observe that move
4 consists of pushing the diagram's upper arc upwards beyond "$\infty$".
\qed
\end{proof}
\begin{figure}[htb]
\begin{picture}(8,9.5)
\thicklines
\put(-0.2,7.5){\knot G}
\put(2.85,7.8){\line(0,1){0.45}}
\put(2.85,7.8){\line(1,0){0.25}}
\put(3.8,7.9){$\longrightarrow$}
\put(4,8.1){\small 1}
\put(4.4,7.5){\knot y}
\put(7.45,7.8){\line(0,1){0.45}}
\put(7.45,7.8){\line(1,0){0.25}}
\put(8.4,7.9){$\longrightarrow$}
\put(8.6,8.1){\small 2}
\put(9,7.5){\knot A}
\put(12.05,7.8){\line(0,1){0.1}}
\put(12.05,7.95){\line(0,1){0.1}}
\put(12.05,8.1){\line(0,1){0.1}}
\put(12.05,8.25){\line(1,0){0.1}}
\put(12.2,8.25){\line(1,0){0.1}}
\put(1,3.9){$\longrightarrow$}
\put(1.2,4.1){\small 3}
\put(2.5,3.5){\knot z}
\put(5.55,3.8){\line(0,1){0.1}}
\put(5.55,3.95){\line(0,1){0.1}}
\put(5.55,4.1){\line(0,1){0.1}}
\put(5.55,4.25){\line(1,0){0.1}}
\put(5.7,4.25){\line(1,0){0.1}}
\put(4.7,4.9){\line(0,1){0.15}}
\put(4.7,5.15){\line(0,1){0.15}}
\put(4.7,5.4){\line(0,1){0.15}}
\put(4.7,5.65){\vector(0,1){0.4}}
\put(4.8,6.4){\circle*{0.1}}
\put(5,6.3){$\infty$}
\put(7.7,3.9){$\longrightarrow$}
\put(7.9,4.1){\small 4}
\put(9,4.1){\knot Z}
\put(12.05,4.4){\line(0,1){0.1}}
\put(12.05,4.55){\line(0,1){0.1}}
\put(12.05,4.7){\line(0,1){0.1}}
\put(12.05,4.85){\line(1,0){0.1}}
\put(12.2,4.85){\line(1,0){0.1}}
\put(1,0.9){$\longrightarrow$}
\put(1.2,1.1){\small 5}
\put(2.3,0.5){\knot G}
\put(5.65,1.15){\line(-1,0){0.1}}
\put(5.5,1.15){\line(-1,0){0.1}}
\put(5.35,1.15){\line(-1,0){0.1}}
\put(5.7,1.15){\line(0,-1){0.1}}
\put(5.7,1){\line(0,-1){0.1}}
\multiput(2.3,1)(0.4,0){7}{\line(1,0){0.2}}
\multiput(2.3,1)(0.4,0){7}{\line(1,0){0.2}}
\multiput(5.9,1)(0.4,0){2}{\line(1,0){0.2}}
\put(6.4,0.9){$\circlearrowleft$}
\put(7.3,0.9){$\longrightarrow$}
\put(8.3,0.5){\knot G}
\put(11.7,1.15){\line(0,-1){0.25}}
\put(11.25,0.9){\line(1,0){0.45}}
\end{picture}
\caption{1 = R. II; 2 = flype; 3 = R. VI; 4 = planar isotopy; 5 = R. II}
\label{picproof}
\end{figure}

Now let $D$ and $D'$ be ambient isotopic diagrams which fulfil the
assumptions of Theorem \ref{main}. Of course, if the corresponding
graph has no vertices then the statement follows from Theorem
\ref{rigidflype}.

For the induction step, an arbitrary graph vertex of $D$ and the
corresponding vertex of $D'$ are replaced with a crossing each such that
the diagrams arising, which shall be denoted by $D_1$ and $D'_1$
respectively, are alternating. Then it follows from Corollary
\ref{trafocor} and the induction hypothesis that $D_1$ and $D'_1$ are
rigid vertex isotopic and thus can be connected by a finite sequence of
flypes, by Theorem \ref{rigidflype}.

Considering the defining Fig. \ref{flype}, there are three different
types of flype that can be applied to $D_1$: either the substituted
crossing lies outside the depicted part of the diagram, or it lies
inside the tangle $t$, or it is identical to the crossing next to $t$.
Call the latter one {\em essential\/} flype. Because of the obvious
one-to-one correspondence between the crossings before and after
applying a flype it is possible to keep track of the substituted
crossing during the whole sequence of flypes connecting $D_1$ and
$D'_1$. Obviously, if the sequence contains no essential flypes then it
gives rise to a sequence of flypes that can be applied to the diagram
$D$ and has $D'$ as final diagram, and the induction step is done.

Now assume that the flyping sequence contains an essential flype. Since
$D$ is prime, cutting open the substituted crossing in either way must
yield a prime graph diagram, and therefore an essential flype can,
essentially, only be applied to $D_1$ as depicted in the first two
pictures of Fig. \ref{finalpic},
\begin{figure}[htb]
\begin{picture}(13,2.5)
\thicklines
\put(0,0.5){\knot E}
\put(3.05,0.8){\line(0,1){0.45}}
\put(3.05,0.8){\line(1,0){0.25}}
\put(4.1,0.9){$\longrightarrow$}
\put(4.3,1.1){\small 1}
\put(5,0.5){\knot D}
\put(5.7,0.8){\line(0,1){0.1}}
\put(5.7,0.95){\line(0,1){0.1}}
\put(5.7,1.1){\line(0,1){0.1}}
\put(5.7,1.25){\line(1,0){0.1}}
\put(5.85,1.25){\line(1,0){0.1}}
\multiput(7.1,-0.25)(0,0.4){7}{\line(0,1){0.2}}
\put(6.95,2.3){$\circlearrowleft$}
\put(9,0.9){$\longrightarrow$}
\put(9.2,1.1){\small 2}
\put(9.7,0.5){\knot E}
\put(13,0.8){\line(0,1){0.45}}
\put(12.75,1.25){\line(1,0){0.25}}
\end{picture}
\caption{1 = flype; 2 = rotation around dashed axis}
\label{finalpic}
\end{figure}
i.e., the whole diagram is involved in the flyping move. Applying Lemma
\ref{rot} twice shows that there arise rigid vertex isotopic diagrams
from re-inserting vertices for crossings in first and last diagram of
Fig. \ref{finalpic}. Therefore an essential flype applied to $D_1$ is
related to a rigid vertex isotopy of the diagram $D$, and an induction
on the number of essential flypes in the flyping sequence completes the
proof of Theorem \ref{main}.


text:
:: Groups
::  by Wojciech A. Trybulec

environ

 vocabularies NUMBERS, NAT_1, INT_1, XBOOLE_0, ALGSTR_0, SUBSET_1, BINOP_2,
      RELAT_1, REAL_1, ARYTM_3, CARD_1, ARYTM_1, BINOP_1, STRUCT_0, FUNCT_1,
      SETWISEO, FINSEQOP, ZFMISC_1, NEWTON, COMPLEX1, XXREAL_0, FINSET_1,
      TARSKI, RLVECT_1, SUPINF_2, GROUP_1, ORDINAL1;
 notations TARSKI, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, RELAT_1, FUNCT_1, XREAL_0, FUNCT_2, BINOP_2, BINOP_1, STRUCT_0,
      ALGSTR_0, RLVECT_1, INT_1, NAT_1, FINSEQOP, SETWISEO, INT_2;
 constructors BINOP_1, SETWISEO, XXREAL_0, REAL_1, NAT_1, NAT_D, BINOP_2,
      FINSEQOP, RLVECT_1;
 registrations ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1,
      STRUCT_0, ALGSTR_0, CARD_1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions FUNCT_2, BINOP_1, FINSEQOP, RLVECT_1, SETWISEO, ALGSTR_0;
 equalities BINOP_1, STRUCT_0, ALGSTR_0;
 expansions BINOP_1, FINSEQOP;
 theorems ABSVALUE, BINOP_1, CARD_1, FINSEQOP, INT_1, NAT_1, ZFMISC_1, BINOP_2,
      XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, NAT_D, XREAL_0;
 schemes FUNCT_2, INT_1, NAT_1, CLASSES1;

begin

reserve m,n for Nat;
reserve i,j for Integer;
reserve S for non empty multMagma;
reserve r,r1,r2,s,s1,s2,t,t1,t2 for Element of S;

Lm1: now
  set G = multMagma (# REAL, addreal #);
  thus for h,g,f being Element of G holds h * g * f = h * (g * f)
  proof
    let h,g,f be Element of G;
    reconsider A = h, B = g, C = f as Real;
A1: g * f = B + C by BINOP_2:def 9;
    h * g = A + B by BINOP_2:def 9;
    hence h * g * f = A + B + C by BINOP_2:def 9
      .= A + (B + C)
      .= h * (g * f) by A1,BINOP_2:def 9;
  end;
  reconsider e = 0 as Element of G by XREAL_0:def 1;
  take e;
  let h be Element of G;
  reconsider A = h as Real;
  thus h * e = A + 0 by BINOP_2:def 9
    .= h;
  thus e * h = 0 + A by BINOP_2:def 9
    .= h;
  reconsider g = - A as Element of G by XREAL_0:def 1;
  take g;
  thus h * g = A + (- A) by BINOP_2:def 9
    .= e;
  thus g * h = (- A) + A by BINOP_2:def 9
    .= e;
end;

definition
  let IT be multMagma;

  attr IT is unital means

  ex e being Element of IT st for h being
  Element of IT holds h * e = h & e * h = h;
  attr IT is Group-like means
  :Def2:
  ex e being Element of IT st for h being
Element of IT holds h * e = h & e * h = h & ex g being Element of IT st h * g =
  e & g * h = e;
  attr IT is associative means
  :Def3:
  for x,y,z being Element of IT holds (x*y )*z = x*(y*z);
end;

registration
  cluster Group-like -> unital for multMagma;
  coherence;
end;

registration
  cluster strict Group-like associative non empty for multMagma;
  existence
  proof
    multMagma (# REAL, addreal #) is Group-like associative by Lm1;
    hence thesis;
  end;
end;

definition
  mode Group is Group-like associative non empty multMagma;
end;

theorem
  ((for r,s,t holds (r * s) * t = r * (s * t)) & ex t st for s1 holds s1
* t = s1 & t * s1 = s1 & ex s2 st s1 * s2 = t & s2 * s1 = t) implies S is Group
  by Def2,Def3;

theorem
  (for r,s,t holds r * s * t = r * (s * t)) & (for r,s holds (ex t st r
  * t = s) & (ex t st t * r = s)) implies S is associative Group-like
proof
  set r = the Element of S;
  assume that
A1: for r,s,t holds r * s * t = r * (s * t) and
A2: for r,s holds (ex t st r * t = s) & ex t st t * r = s;
  consider s1 such that
A3: r * s1 = r by A2;
  thus for r,s,t holds r * s * t = r * (s * t) by A1;
  take s1;
  let s;
  ex t st t * r = s by A2;
  hence
A4: s * s1 = s by A1,A3;
  consider s2 such that
A5: s2 * r = r by A2;
  consider t1 such that
A6: r * t1 = s1 by A2;
A7: ex t2 st t2 * r = s2 by A2;
A8: s1 = s2 * (r * t1) by A1,A5,A6
    .= s2 by A1,A3,A6,A7;
  ex t st r * t = s by A2;
  hence
A9: s1 * s = s by A1,A5,A8;
  consider t1 such that
A10: s * t1 = s1 by A2;
  consider t2 such that
A11: t2 * s = s1 by A2;
  take t1;
  consider r1 such that
A12: s * r1 = t1 by A2;
A13: ex r2 st r2 * s = t2 by A2;
  t1 = s1 * (s * r1) by A1,A9,A12
    .= t2 * (s * t1) by A1,A11,A12
    .= t2 by A1,A4,A10,A13;
  hence thesis by A10,A11;
end;

theorem Th3:
  multMagma (# REAL, addreal #) is associative Group-like
proof
  set G = multMagma (# REAL, addreal #);
  thus for h,g,f being Element of G holds h * g * f = h * (g * f)
  proof
    let h,g,f be Element of G;
    reconsider A = h, B = g, C = f as Real;
A1: g * f = B + C by BINOP_2:def 9;
    h * g = A + B by BINOP_2:def 9;
    hence h * g * f = A + B + C by BINOP_2:def 9
      .= A + (B + C)
      .= h * (g * f) by A1,BINOP_2:def 9;
  end;
  reconsider e = 0 as Element of G by XREAL_0:def 1;
  take e;
  let h be Element of G;
  reconsider A = h as Real;
  thus h * e = A + 0 by BINOP_2:def 9
    .= h;
  thus e * h = 0 + A by BINOP_2:def 9
    .= h;
  reconsider g = - A as Element of G by XREAL_0:def 1;
  take g;
  thus h * g = A + (- A) by BINOP_2:def 9
    .= e;
  thus g * h = (- A) + A by BINOP_2:def 9
    .= e;
end;

reserve G for Group-like non empty multMagma;
reserve e,h for Element of G;

definition
  let G be multMagma such that
A1: G is unital;
  func 1_G -> Element of G means
  :Def4:
  for h being Element of G holds h * it = h & it * h = h;
  existence by A1;
  uniqueness
  proof
    let e1,e2 be Element of G;
    assume that
A2: for h being Element of G holds h * e1 = h & e1 * h = h and
A3: for h being Element of G holds h * e2 = h & e2 * h = h;
    thus e1 = e2 * e1 by A3
      .= e2 by A2;
  end;
end;

theorem
  (for h holds h * e = h & e * h = h) implies e = 1_G by Def4;

reserve G for Group;
reserve f,g,h for Element of G;

definition
  let G,h;
  func h" -> Element of G means
  :Def5:
  h * it = 1_G & it * h = 1_G;
  existence
  proof
    consider e being Element of G such that
A1: for h being Element of G holds h * e = h & e * h = h & ex g being
    Element of G st h * g = e & g * h = e by Def2;
    consider g being Element of G such that
A2: h * g = e & g * h = e by A1;
    take g;
    thus thesis by A1,A2,Def4;
  end;
  uniqueness
  proof
    let h1,h2 be Element of G;
    assume that
A3: h * h1 = 1_G and
    h1 * h = 1_G and
    h * h2 = 1_G and
A4: h2 * h = 1_G;
    thus h1 = 1_G * h1 by Def4
      .= h2 * (h * h1) by A4,Def3
      .= h2 by A3,Def4;
  end;
  involutiveness;
end;

theorem
  h * g = 1_G & g * h = 1_G implies g = h" by Def5;

theorem Th6:
  h * g = h * f or g * h = f * h implies g = f
proof
  assume h * g = h * f or g * h = f * h;
  then h" * (h * g) = h" * h * f or g * h * h" = f * (h * h") by Def3;
  then h" * (h * g) = 1_G * f or g * (h * h") = f * (h * h") by Def3,Def5;
  then h" * (h * g) = f or g * 1_G = f * (h * h") by Def4,Def5;
  then h" * h * g = f or g = f * (h * h") by Def3,Def4;
  then h" * h * g = f or g = f * 1_G by Def5;
  then 1_G * g = f or g = f by Def4,Def5;
  hence thesis by Def4;
end;

theorem
  h * g = h or g * h = h implies g = 1_G
proof
  h * 1_G = h & 1_G * h = h by Def4;
  hence thesis by Th6;
end;

theorem Th8:
  (1_G)" = 1_G
proof
  (1_G)" * 1_G = 1_G by Def5;
  hence thesis by Def4;
end;

theorem
  h" = g" implies h = g
proof
  assume h" = g";
  then
A1: h * g" = 1_G by Def5;
  g * g" = 1_G by Def5;
  hence thesis by A1,Th6;
end;

theorem
  h" = 1_G implies h = 1_G
proof
  (1_G)" = 1_G by Th8;
  hence thesis;
end;

::$CT

theorem Th11:
  h * g = 1_G implies h = g" & g = h"
proof
  assume
A1: h * g = 1_G;
  h * h" = 1_G & g" * g = 1_G by Def5;
  hence thesis by A1,Th6;
end;

theorem Th12:
  h * f = g iff f = h" * g
proof
  h * (h" * g) = h * h" * g by Def3
    .= 1_G * g by Def5
    .= g by Def4;
  hence h * f = g implies f = h" * g by Th6;
  assume f = h" * g;
  hence h * f = h * h" * g by Def3
    .= 1_G * g by Def5
    .= g by Def4;
end;

theorem Th13:
  f * h = g iff f = g * h"
proof
  g * h" * h = g * (h" * h) by Def3
    .= g * 1_G by Def5
    .= g by Def4;
  hence f * h = g implies f = g * h" by Th6;
  assume f = g * h";
  hence f * h = g * (h" * h) by Def3
    .= g * 1_G by Def5
    .= g by Def4;
end;

theorem
  ex f st g * f = h
proof
  take g" * h;
  thus thesis by Th12;
end;

theorem
  ex f st f * g = h
proof
  take h * g";
  thus thesis by Th13;
end;

theorem Th16:
  (h * g)" = g" * h"
proof
  (g" * h") * (h * g) = g" * h" * h * g by Def3
    .= g" * (h" * h) * g by Def3
    .= g" * 1_G * g by Def5
    .= g" * g by Def4
    .= 1_G by Def5;
  hence thesis by Th11;
end;

theorem Th17:
  g * h = h * g iff (g * h)" = g" * h"
proof
  thus g * h = h * g implies (g * h)" = g" * h" by Th16;
  assume (g * h)" = g" * h";
  then
A1: (h * g) * (g * h)" = h * g * g" * h" by Def3
    .= h * (g * g") * h" by Def3
    .= h * 1_G * h" by Def5
    .= h * h" by Def4
    .= 1_G by Def5;
  (g * h) * (g * h)" = 1_G by Def5;
  hence thesis by A1,Th6;
end;

theorem Th18:
  g * h = h * g iff g" * h" = h" * g"
proof
  thus g * h = h * g implies g" * h" = h" * g"
  proof
    assume
A1: g * h = h * g;
    hence g" * h" = (g * h)" by Th16
      .= h" * g" by A1,Th17;
  end;
  assume
A2: g" * h" = h" * g";
  thus g * h = (g * h)"" .= (h" * g")" by Th16
    .= h"" * g"" by A2,Th16
    .= h * g;
end;

theorem Th19:
  g * h = h * g iff g * h" = h" * g
proof
  thus g * h = h * g implies g * h" = h" * g
  proof
    assume
A1: g * h = h * g;
    (g * h") * (g" * h) = g * h" * g" * h by Def3
      .= g * (h" * g") * h by Def3
      .= g * (g" * h") * h by A1,Th18
      .= g * g" * h" * h by Def3
      .= 1_G * h" * h by Def5
      .= h" * h by Def4
      .= 1_G by Def5;
    then g * h" = (g" * h)" by Th11
      .= h" * g"" by Th16;
    hence thesis;
  end;
  assume g * h" = h" * g;
  then g * (h" * h) = h" * g * h by Def3;
  then g * 1_G = h" * g * h by Def5;
  then g = h" * g * h by Def4;
  then g = h" * (g * h) by Def3;
  then h * g = h * h" * (g * h) by Def3;
  then h * g = 1_G * (g * h) by Def5;
  hence thesis by Def4;
end;

reserve u for UnOp of G;

definition
  let G;
  func inverse_op(G) -> UnOp of G means
  :Def6:
  it.h = h";
  existence
  proof
    deffunc F(Element of G) = $1";
    consider u such that
A1: for h being Element of G holds u.h = F(h) from FUNCT_2:sch 4;
    take u;
    let h;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let u1,u2 be UnOp of G;
    assume
A2: for h holds u1.h = h";
    assume
A3: for h holds u2.h = h";
    let h be Element of G;
    thus u1.h = h" by A2
      .= u2.h by A3;
  end;
end;

registration
  let G be associative non empty multMagma;
  cluster  the multF of G -> associative;
  coherence
proof
  let h,g,f be Element of G;
  set o = the multF of G;
  thus o.(h,o.(g,f)) = h * (g * f) .= h * g * f by Def3
    .= o.(o.(h,g),f);
end;
end;

theorem Th20:
  for G being unital non empty multMagma holds 1_G is_a_unity_wrt
  the multF of G
proof
  let G be unital non empty multMagma;
  set o = the multF of G;
  now
    let h be Element of G;
    thus o.(1_G,h) = 1_G * h .= h by Def4;
    thus o.(h,1_G) = h * 1_G .= h by Def4;
  end;
  hence thesis by BINOP_1:3;
end;

theorem Th21:
  for G being unital non empty multMagma holds the_unity_wrt the
  multF of G = 1_G
proof
  let G be unital non empty multMagma;
  1_G is_a_unity_wrt the multF of G by Th20;
  hence thesis by BINOP_1:def 8;
end;

registration
  let G be unital non empty multMagma;
  cluster the multF of G -> having_a_unity;
coherence
proof
  take 1_G;
  thus thesis by Th20;
end;
end;

theorem Th22:
  inverse_op(G) is_an_inverseOp_wrt the multF of G
proof
  let h be Element of G;
  thus (the multF of G).(h,inverse_op(G).h) = h * h" by Def6
    .= 1_G by Def5
    .= the_unity_wrt the multF of G by Th21;
  thus (the multF of G).(inverse_op(G).h,h) = h" * h by Def6
    .= 1_G by Def5
    .= the_unity_wrt the multF of G by Th21;
end;

registration
  let G;
  cluster the multF of G -> having_an_inverseOp;
  coherence
proof
  inverse_op(G) is_an_inverseOp_wrt the multF of G by Th22;
  hence thesis;
end;
end;

theorem
  the_inverseOp_wrt the multF of G = inverse_op(G)
proof
  set o = the multF of G;
  o is having_an_inverseOp & inverse_op(G) is_an_inverseOp_wrt o by Th22;
  hence thesis by FINSEQOP:def 3;
end;

definition
  let G be non empty multMagma;
  func power G -> Function of [:the carrier of G,NAT:], the carrier of G means
  :Def7:
  for h being Element of G holds it.(h,0) = 1_G &
   for n being Nat holds it.(h,n + 1) = it.(h,n) * h;
  existence
  proof
    defpred P[object,object] means
ex g0 being sequence of  the carrier of G, h
being Element of G st $1 = h & g0 = $2 & g0.0 = 1_G & for n holds g0.(n + 1) =
    (g0.n) * h;
A1: for x be object st x in the carrier of G ex y be object st P[x,y]
    proof
      let x be object;
      assume x in the carrier of G;
      then reconsider b = x as Element of G;
      deffunc F(Nat,Element of G) = $2 * b;
      consider g0 being sequence of  the carrier of G such that
A2:   g0.0 = 1_G and
A3:   for n being Nat holds g0.(n + 1) = F(n,g0.n) from NAT_1:sch 12;
      reconsider y = g0 as set;
      take y;
      take g0;
      take b;
      thus x = b & g0 = y & g0.0 = 1_G by A2;
      let n;
      thus thesis by A3;
    end;
    consider f being Function such that
    dom f = the carrier of G and
A4: for x be object st x in the carrier of G holds P[x,f.x] from CLASSES1
    :sch 1(A1);
    defpred P[Element of G,Nat,set] means ex g0 being sequence of
    the carrier of G st g0 = f.$1 & $3 = g0.$2;
A5: for a being Element of G, n being Nat ex b being Element of
    G st P[a,n,b]
    proof
      let a be Element of G, n be Nat;
      consider g0 being sequence of  the carrier of G, h being Element of
      G such that
      a = h and
A6:   g0 = f.a and
      g0.0 = 1_G and
      for n holds g0.(n + 1) = (g0.n) * h by A4;
      take g0.n, g0;
      thus thesis by A6;
    end;
    consider F being Function of [:the carrier of G,NAT:], the carrier of G
    such that
A7: for a being Element of G, n being Nat holds P[a,n,F.(a,n)]
      from NAT_1:sch 19(A5);
    take F;
    let h be Element of G;
A8: ex g2 being sequence of  the carrier of G, b being Element of G
st h = b & g2 = f.h & g2.0 = 1_G & for n holds g2.(n + 1) = (g2.n) * b by A4;
    ex g1 being sequence of  the carrier of G st g1 = f.h & F.(h,0) =
    g1.0 by A7;
    hence F.(h,0) = 1_G by A8;
    let n be Nat;
A9: ex g2 being sequence of  the carrier of G, b being Element of G st
    h = b & g2 = f.h & g2.0 = 1_G & for n holds g2.(n + 1) = ( g2.n) * b by A4;
    ( ex g0 being sequence of  the carrier of G st g0 = f.h & F.(h,n)
= g0.n)& ex g1 being sequence of  the carrier of G st g1 = f.h & F.(h,n + 1
    ) = g1.(n + 1) by A7;
    hence thesis by A9;
  end;
  uniqueness
  proof
    let f,g be Function of [:the carrier of G,NAT:], the carrier of G;
    assume that
A10: for h being Element of G holds f.(h,0) = 1_G & for n being Nat
      holds f.(h,n + 1) = (f.(h,n)) * h and
A11: for h being Element of G holds g.(h,0) = 1_G & for n being Nat
     holds g.(h,n + 1) = (g.(h,n)) * h;
    now
      let h be Element of G, n be Element of NAT;
      defpred P[Nat] means f.[h,$1] = g.[h,$1];
A12:  now
        let n be Nat;
        assume
A13:    P[n];
A14:    g.[h,n] = g.(h,n);
        f.[h,n + 1] = f.(h,n + 1) .= (f.(h,n)) * h by A10
          .= g.(h,n + 1) by A11,A13,A14
          .= g.[h,n + 1];
        hence P[n+1];
      end;
      f.[h,0] = f.(h,0) .= 1_G by A10
        .= g.(h,0) by A11
        .= g.[h,0];
      then
A15:  P[0];
      for n being Nat holds P[n] from NAT_1:sch 2(A15,A12);
      hence f.(h,n) = g.(h,n);
    end;
    hence thesis;
  end;
end;

definition
  let G,h; let i be Integer;
  func h |^ i -> Element of G equals
  :Def8:
  power(G).(h,|.i.|) if 0 <= i
  otherwise (power(G).(h,|.i.|))";
  correctness;
end;

definition
  let G,h; let n be natural Number;
  redefine func h |^ n equals
  power(G).(h,n);
  compatibility
  proof
    let g be Element of G;
    |.n.| = n by ABSVALUE:def 1;
    hence thesis by Def8;
  end;
end;

Lm2: h |^ (n + 1) = h |^ n * h
by Def7;

Lm3: h |^ 0 = 1_G by Def7;

Lm4: (1_G) |^ n = 1_G
proof
  defpred P[Nat] means (1_G) |^ $1 = 1_G;
A1: now
    let n;
    assume P[n];
    then (1_G) |^ (n + 1) = 1_G * 1_G by Lm2
      .= 1_G by Def4;
    hence P[n+1];
  end;
A2: P[0] by Def7;
  for n holds P[n] from NAT_1:sch 2(A2,A1);
  hence thesis;
end;

theorem
  h |^ 0 = 1_G by Def7;

theorem Th25:
  h |^ 1 = h
proof
  thus h |^ 1 = h |^(0 + 1) .= h |^ 0 * h by Lm2
    .= 1_G * h by Def7
    .= h by Def4;
end;

theorem Th26:
  h |^ 2 = h * h
proof
  thus h |^ 2 = h |^ (1 + 1) .= h |^ 1 * h by Lm2
    .= h * h by Th25;
end;

theorem
  h |^ 3 = h * h * h
proof
  thus h |^ 3 = h |^ (2 + 1) .= h |^ 2 * h by Lm2
    .= h * h * h by Th26;
end;

theorem
  h |^ 2 = 1_G iff h" = h
proof
  thus h |^ 2 = 1_G implies h = h"
  proof
    assume h |^ 2 = 1_G;
    then h * h = 1_G by Th26;
    hence thesis by Th11;
  end;
  assume h = h";
  hence h |^ 2 = h * h" by Th26
    .= 1_G by Def5;
end;

Lm5: h |^ (n + m) = h |^ n * (h |^ m)
proof
  defpred P[Nat] means for n holds h |^ (n + $1) = h |^ n * (h |^ $1);
A1: for m st P[m] holds P[m+1]
  proof
    let m;
    assume
A2: for n holds h |^ (n + m) = h |^ n * (h |^ m);
    let n;
    thus h |^ (n + (m + 1)) = h |^ (n + m + 1) .= h |^ (n + m) * h by Lm2
      .= h |^ n * (h |^ m) * h by A2
      .= h |^ n * (h |^ m * h) by Def3
      .= h |^ n * (h |^ (m + 1)) by Lm2;
  end;
A3: P[0]
  proof
    let n;
    thus h |^ (n + 0) = h |^ n * 1_G by Def4
      .= h |^ n * (h |^ 0) by Def7;
  end;
  for m holds P[m] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

Lm6: h |^ (n + 1) = h |^ n * h & h |^ (n + 1) = h * (h |^ n)
proof
  thus h |^ (n + 1) = h |^ n * h by Lm2;
  thus h |^ (n + 1) = h |^ 1 * (h |^ n) by Lm5
    .= h * (h |^ n) by Th25;
end;

Lm7: h |^ (n * m) = h |^ n |^ m
proof
  defpred P[Nat] means for n holds h |^ (n * $1) = h |^ n |^ $1;
A1: for m st P[m] holds P[m+1]
  proof
    let m;
    assume
A2: for n holds h |^ (n * m) = h |^ n |^ m;
    let n;
    thus h |^ (n * (m + 1)) = h |^ (n * m + n * 1)
      .= h |^ (n * m) * (h |^ n) by Lm5
      .= h |^ n |^ m * (h |^ n) by A2
      .= h |^ n |^ m * (h |^ n |^ 1) by Th25
      .= h |^ n |^ (m + 1) by Lm5;
  end;
A3: P[0]
  proof
    let n;
    thus h |^ (n * 0) = 1_G by Def7
      .= h |^ n |^ 0 by Def7;
  end;
  for m holds P[m] from NAT_1:sch 2(A3,A1);
  hence thesis;
end;

Lm8: h" |^ n = (h |^ n)"
proof
  defpred P[Nat] means h" |^ $1 = (h |^ $1)";
A1: now
    let n;
    assume P[n];
    then h" |^ (n + 1) = (h |^ n)" * h" by Lm2
      .= (h * (h |^ n))" by Th16
      .= (h |^ (n + 1))" by Lm6;
    hence P[n+1];
  end;
  h" |^ 0 = 1_G by Def7
    .= (1_G)" by Th8
    .= (h |^ 0)" by Def7;
  then
A2: P[0];
  for n holds P[n] from NAT_1:sch 2(A2,A1);
  hence thesis;
end;

Lm9: g * h = h * g implies g * (h |^ n) = h |^ n * g
proof
  defpred P[Nat] means g * h = h * g implies g * (h |^ $1) = h |^ $1 * g;
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: g * h = h * g implies g * (h |^ n) = h |^ n * g;
    assume
A3: g * h = h * g;
    thus g * (h |^ (n + 1)) = g * (h * (h |^ n)) by Lm6
      .= g * h * (h |^ n) by Def3
      .= h * ((h |^ n) * g)by A2,A3,Def3
      .= h * (h |^ n) * g by Def3
      .= h |^ (n + 1) * g by Lm6;
  end;
A4: P[0]
  proof
    assume g * h = h * g;
    thus g * (h |^ 0) = g * 1_G by Def7
      .= g by Def4
      .= 1_G * g by Def4
      .= h |^ 0 * g by Def7;
  end;
  for n holds P[n] from NAT_1:sch 2(A4,A1);
  hence thesis;
end;

Lm10: g * h = h * g implies g |^ n * (h |^ m) = h |^ m * (g |^ n)
proof
  defpred P[Nat] means for m st g * h = h * g holds g |^ $1 * (h |^ m) = h |^
  m * (g |^ $1);
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: for m st g * h = h * g holds g |^ n * (h |^ m) = h |^ m * (g |^ n);
    let m;
    assume
A3: g * h = h * g;
    thus g |^ (n + 1) * (h |^ m) = g * (g |^ n) * (h |^ m) by Lm6
      .= g * ((g |^ n) * (h |^ m)) by Def3
      .= g * ((h |^ m) * (g |^ n)) by A2,A3
      .= g * (h |^ m) * (g |^ n) by Def3
      .= h |^ m * g * (g |^ n) by A3,Lm9
      .= h |^ m * (g * (g |^ n)) by Def3
      .= h |^ m * (g |^ (n + 1)) by Lm6;
  end;
A4: P[0]
  proof
    let m;
    assume g * h = h * g;
    thus g |^ 0 * (h |^ m) = 1_G * (h |^ m)by Def7
      .= h |^ m by Def4
      .= h |^ m * 1_G by Def4
      .= h |^ m * (g |^ 0) by Def7;
  end;
  for n holds P[n] from NAT_1:sch 2(A4,A1);
  hence thesis;
end;

Lm11: g * h = h * g implies (g * h) |^ n = g |^ n * (h |^ n)
proof
  defpred P[Nat] means g * h = h * g implies (g * h) |^ $1 = g |^ $1 * (h |^
  $1);
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: g * h = h * g implies (g * h) |^ n = g |^ n * (h |^ n);
    assume
A3: g * h = h * g;
    hence (g * h) |^ (n + 1) = g |^ n * (h |^ n) * (h * g) by A2,Lm6
      .= g |^ n * (h |^ n) * h * g by Def3
      .= g |^ n * ((h |^ n) * h) * g by Def3
      .= g |^ n * (h |^ (n + 1)) * g by Lm6
      .= h |^ (n + 1) * (g |^ n) * g by A3,Lm10
      .= h |^ (n + 1) * ((g |^ n) * g) by Def3
      .= h |^ (n + 1) * (g |^ (n + 1)) by Lm6
      .= g |^ (n + 1) * (h |^ (n + 1)) by A3,Lm10;
  end;
A4: P[0]
  proof
    assume g * h = h * g;
    thus (g * h) |^ 0 = 1_G by Def7
      .= 1_G * 1_G by Def4
      .= g |^ 0 * 1_G by Def7
      .= g |^ 0 * (h |^ 0) by Def7;
  end;
  for n holds P[n] from NAT_1:sch 2(A4,A1);
  hence thesis;
end;

theorem Th29:
  i <= 0 implies h |^ i = (h |^ |.i.|)"
proof
  assume
A1: i <= 0;
  per cases by A1;
  suppose
    i < 0;
    hence thesis by Def8;
  end;
  suppose
A2: i = 0;
    hence h |^ i = 1_G by Lm3
      .= (1_G)" by Th8
      .= (h |^ 0)" by Def7
      .= (h |^ |.i.|)" by A2,ABSVALUE:def 1;
  end;
end;

theorem
  (1_G) |^ i = 1_G
proof
  (1_G) |^ i = (1_G) |^ |.i.| or (1_G) |^ i = ((1_G) |^ |.i.|)" & (1_G)"
  = 1_G by Def8,Th8;
  hence thesis by Lm4;
end;

theorem Th31:
  h |^ (-1) = h"
proof
  |.-1.| = - (-1) by ABSVALUE:def 1;
  hence h |^ (-1) = (h |^ 1)" by Def8
    .= h" by Th25;
end;

Lm12: h |^ (- i) = (h |^ i)"
proof
  per cases;
  suppose
A1: i >= 0;
    per cases by A1,XREAL_1:24;
    suppose
A2:   - i < -0;
      hence h |^ (- i) = (h |^ |.- i .|)" by Def8
        .= (h |^ (- (- i)))" by A2,ABSVALUE:def 1
        .= (h |^ i)";
    end;
    suppose
A3:   i = 0;
      hence h |^ (- i) = 1_G by Lm3
        .= (1_G)" by Th8
        .= (h |^ i)" by A3,Lm3;
    end;
  end;
  suppose
A4: i < 0;
    then h |^ i = (h |^ |.i.|)" by Def8;
    hence thesis by A4,ABSVALUE:def 1;
  end;
end;

Lm13: j >= 1 or j = 0 or j < 0
proof
  j < 0 or j is Element of NAT & (j <> 0 or j = 0) by INT_1:3;
  hence thesis by NAT_1:14;
end;

Lm14: h |^ (j - 1) = h |^ j * (h |^ (-1))
proof
A1: now
    per cases by Lm13;
    suppose
A2:   j >= 1;
      then j >= 1 + 0;
      then
A3:   j - 1 >= 0 by XREAL_1:19;
      then
A4:   |.j-1.| + 1 = j - 1 + 1 by ABSVALUE:def 1
        .= j;
A5:   |.j.| = j by A2,ABSVALUE:def 1;
A6:   |.j.| = |.-j.| by COMPLEX1:52;
      thus h|^(j - 1) * (h * (h|^(- j))) = h|^(j - 1) * h * (h|^(- j)) by Def3
        .= h |^ |.j-1.| * h * (h |^ (- j)) by A3,Def8
        .= h |^ |.j-1.| * h * ((h |^ |.-j.|)") by A2,Th29
        .= h |^ (|.j-1.| + 1) * ((h |^ |.-j.|)") by Lm6
        .= 1_G by A4,A5,A6,Def5;
    end;
    suppose
A7:   j < 0;
A8:   1 - j = - (j - 1);
      thus h |^ (j - 1) * (h * (h |^ (- j))) = (h |^ |.j-1.|)" * (h * (h
      |^ (- j))) by A7,Def8
        .= (h |^ |.j-1.|)" * (h * (h |^ |.-j.|)) by A7,Def8
        .= (h |^ |.j-1.|)" * (h |^ (1 + |.-j.|)) by Lm6
        .= (h |^ |.j-1.|)" * (h |^ (1 + (- j))) by A7,ABSVALUE:def 1
        .= (h |^ |.j-1.|)" * (h |^ |.j-1.|) by A7,A8,ABSVALUE:def 1
        .= 1_G by Def5;
    end;
    suppose
A9:   j = 0;
      hence h |^ (j - 1) * (h * (h |^ (- j))) = h" * (h * (h |^ (- j))) by Th31
        .= h " * h * (h |^ (- j)) by Def3
        .= 1_G * (h |^ (- j)) by Def5
        .= h |^ 0 by A9,Def4
        .= 1_G by Def7;
    end;
  end;
  h|^(j - 1) * (h|^(1 - j)) = h|^(j - 1) * (h|^(- (j - 1)))
    .= h |^ (j - 1) * (h |^ (j - 1))" by Lm12
    .= 1_G by Def5;
  then h * (h |^ (- j)) = h |^ (1 - j) by A1,Th6;
  then (h |^ (1 - j))" = (h |^ (- j))" * h" by Th16
    .= (h |^ (- (- j))) * h" by Lm12
    .= h |^ j * (h |^ (-1)) by Th31;
  then h |^ j * (h |^ (-1)) = h |^ (- (1 - j)) by Lm12;
  hence thesis;
end;

Lm15: j >= 0 or j = - 1 or j < - 1
proof
  per cases;
  suppose
    j >= 0;
    hence thesis;
  end;
  suppose
A1: j < 0;
    then reconsider n = - j as Element of NAT by INT_1:3;
    n <> -0 by A1;
    then n >= 1 by NAT_1:14;
    then n > 1 or n = 1 by XXREAL_0:1;
    then - 1 > - (- j) or - 1 = j by XREAL_1:24;
    hence thesis;
  end;
end;

Lm16: h |^ (j + 1) = h |^ j * (h |^ 1)
proof
A1: now
    per cases by Lm15;
    suppose
A2:   j >= 0;
      then reconsider n = j as Element of NAT by INT_1:3;
A3:   n + 1 = |.j+1.| by ABSVALUE:def 1;
      n + 1 >= 0;
      hence
      h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = h |^ |.j+1.| * (
      (h |^ (-1)) * (h |^ (- j))) by Def8
        .= h |^ |.j+1.| * (h" * (h |^ (- j))) by Th31
        .= h |^ |.j+1.| * (h" * (h |^ j)") by Lm12
        .= h |^ |.j+1.| * (h" * (h |^ |.j.|)") by A2,Def8
        .= h |^ |.j+1.| * ((h |^ |.j.| * h)") by Th16
        .= h |^ |.j+1.| * (h |^ (|.j.| + 1))" by Lm6
        .= h |^ |.j+1.| * (h |^ |.j+1.|)" by A3,ABSVALUE:def 1
        .= 1_G by Def5;
    end;
    suppose
      j < - 1;
      then
A4:   j + 1 < - 1 + 1 by XREAL_1:6;
      hence h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = (h |^ |.j+1.|)"
      * ((h |^ (-1)) * (h |^ (- j))) by Def8
        .= (h |^ |.j+1.|)" * (h" * (h |^ (- j))) by Th31
        .= (h |^ |.j+1.|)" * h" * (h |^ (- j)) by Def3
        .= (h * (h |^ |.j+1.|))" * (h |^ (- j)) by Th16
        .= (h |^ (|.j+1.| + 1))" * (h |^ (- j)) by Lm6
        .= (h |^ (- (j + 1) + 1))" * (h |^ (- j)) by A4,ABSVALUE:def 1
        .= 1_G by Def5;
    end;
    suppose
A5:   j = - 1;
      hence h |^ (j + 1) * ((h |^ (-1)) * (h |^ (- j))) = 1_G * ((h |^ (-1)) *
      (h |^ (- j))) by Lm3
        .= (h |^ (-1)) * (h |^ (- j)) by Def4
        .= h" * (h |^ (- j)) by Th31
        .= h" * (h |^ j)" by Lm12
        .= h" * h"" by A5,Th31
        .= 1_G by Def5;
    end;
  end;
  h |^ (j + 1) * (h |^ (- (j + 1))) = h |^ (j + 1) * (h |^ (j + 1))" by Lm12
    .= 1_G by Def5;
  then
A6: h |^ (- (j + 1)) = h |^ (-1) * (h |^ (- j)) by A1,Th6;
  thus h |^ (j + 1) = h |^ (- (- (j + 1)))
    .= ((h |^ (-1)) * (h |^ (- j)))" by A6,Lm12
    .= (h |^ (- j))" * (h |^ (-1))" by Th16
    .= h |^ (- (- j)) * (h |^ (-1))" by Lm12
    .= h |^ j * (h |^ (- (-1))) by Lm12
    .= h |^ j * (h |^ 1);
end;

theorem Th32:
  h |^ (i + j) = (h |^ i) * (h |^ j)
proof
  defpred P[Integer] means for i holds h |^ (i + $1) = h |^ i * (h |^ $1);
A1: for j holds P[j] implies P[j - 1] & P[j + 1]
  proof
    let j;
    assume
A2: for i holds h |^ (i + j) = h |^ i * (h |^ j);
    thus for i holds h |^ (i + (j - 1)) = h |^ i * (h |^ (j - 1))
    proof
      let i;
      thus h |^ (i + (j - 1)) = h |^ ((i - 1) + j)
        .= h |^ (i - 1) * (h |^ j) by A2
        .= h |^ i * (h |^ (-1)) * (h |^ j) by Lm14
        .= h |^ i * ((h |^ (-1)) * (h |^ j)) by Def3
        .= h |^ i * (h |^ (j + (-1))) by A2
        .= h |^ i * (h |^ (j - 1));
    end;
    let i;
    thus h |^ (i + (j + 1)) = h |^ ((i + 1) + j)
      .= h |^ (i + 1) * (h |^ j) by A2
      .= h |^ i * (h |^ 1) * (h |^ j) by Lm16
      .= h |^ i * ((h |^ 1) * (h |^ j)) by Def3
      .= h |^ i * (h |^ (j + 1)) by A2;
  end;
A3: P[0]
  proof
    let i;
    thus h |^ (i + 0) = h |^ i * 1_G by Def4
      .= h |^ i * (h |^ 0) by Def7;
  end;
  for j holds P[j] from INT_1:sch 4(A3,A1);
  hence thesis;
end;

theorem
  h |^ (i + 1) = h |^ i * h & h |^ (i + 1) = h * (h |^ i)
proof
  h |^ 1 = h by Th25;
  hence thesis by Th32;
end;

Lm17: h" |^ i = (h |^ i)"
proof
  per cases;
  suppose
    i >= 0;
    then reconsider n = i as Element of NAT by INT_1:3;
    thus h" |^ i = (h |^ n)" by Lm8
      .= (h |^ i)";
  end;
  suppose
A1: i < 0;
    hence h" |^ i = (h" |^ |.i.|)" by Def8
      .= (h |^ |.i.|)"" by Lm8
      .= (h |^ i)" by A1,Def8;
  end;
end;

theorem
  h |^ (i * j) = h |^ i |^ j
proof
  per cases;
  suppose
    i >= 0 & j >= 0;
    then reconsider m = i, n = j as Element of NAT by INT_1:3;
    thus h |^ (i * j) = h |^ m |^ n by Lm7
      .= h |^ i |^ j;
  end;
  suppose
    i >= 0 & j < 0;
    then reconsider m = i, n = - j as Element of NAT by INT_1:3;
    i * j = - (i * n);
    hence h |^ (i * j) = (h |^ (i * n))" by Lm12
      .= h" |^ (i * n) by Lm17
      .= h" |^ m |^ n by Lm7
      .= (h |^ i)" |^ n by Lm17
      .= ((h |^ i)" |^ j)" by Lm12
      .= (h |^ i |^ j)"" by Lm17
      .= h |^ i |^ j;
  end;
  suppose
    i < 0 & j >= 0;
    then reconsider m = - i, n = j as Element of NAT by INT_1:3;
    i * j = - (m * j);
    hence h |^ (i * j) = (h |^ (m * j))" by Lm12
      .= h" |^ (m * j) by Lm17
      .= h" |^ m |^ n by Lm7
      .= (h" |^ i)" |^ n by Lm12
      .= (h |^ i)"" |^ j by Lm17
      .= h |^ i |^ j;
  end;
  suppose
    j < 0 & i < 0;
    then reconsider m = - i, n = - j as Element of NAT by INT_1:3;
    i * j * ((-1) * (-1)) = m * n;
    hence h |^ (i * j) = h |^ m |^ n by Lm7
      .= (h |^ (- i) |^ j)" by Lm12
      .= ((h |^ i)" |^ j)" by Lm12
      .= (h" |^ i |^ j)" by Lm17
      .= ((h" |^ i)") |^ j by Lm17
      .= h"" |^ i |^ j by Lm17
      .= h |^ i |^ j;
  end;
end;

theorem
  h |^ -i = (h |^ i)" by Lm12;

theorem
  h" |^ i = (h |^ i)" by Lm17;

theorem Th37:
  g * h = h * g implies (g * h) |^ i = g |^ i * (h |^ i)
proof
  assume
A1: g * h = h * g;
  per cases;
  suppose
A2: i >= 0;
    then
A3: h |^ i = h |^ |.i.| by Def8;
    (g * h) |^ i = (g * h) |^ |.i.| & g |^ i = g |^ |.i.| by A2,Def8;
    hence thesis by A1,A3,Lm11;
  end;
  suppose
A4: i < 0;
    hence (g * h) |^ i = ((h * g) |^ |.i.|)" by A1,Def8
      .= (h |^ |.i.| * (g |^ |.i.|))" by A1,Lm11
      .= (g |^ |.i.|)" * (h |^ |.i.|)" by Th16
      .= g |^ i * (h |^ |.i.|)" by A4,Def8
      .= g |^ i * (h |^ i) by A4,Def8;
  end;
end;

theorem Th38:
  g * h = h * g implies g |^ i * (h |^ j) = h |^ j * (g |^ i)
proof
  assume
A1: g * h = h * g;
  per cases;
  suppose
    i >= 0 & j >= 0;
    then g |^ i = g |^ |.i.| & h |^ j = h |^ |.j.| by Def8;
    hence thesis by A1,Lm10;
  end;
  suppose
A2: i >= 0 & j < 0;
A3: g|^|.i.| * (h|^|.j.|) = h|^|.j.| * (g|^|.i.|) by A1,Lm10;
    g |^ i = g |^ |.i.| & h |^ j = (h |^ |.j.|)" by A2,Def8;
    hence thesis by A3,Th19;
  end;
  suppose
A4: i < 0 & j >= 0;
A5: g|^|.i.| * (h|^|.j.|) = h|^|.j.| * (g|^|.i.|) by A1,Lm10;
    g |^ i = (g |^ |.i.|)" & h |^ j = h |^ |.j.| by A4,Def8;
    hence thesis by A5,Th19;
  end;
  suppose
    i < 0 & j < 0;
    then
A6: g |^ i = (g |^ |.i.|)" & h |^ j = (h |^ |.j.|)" by Def8;
    hence g |^ i * (h |^ j) = (h |^ |.j.| * (g |^ |.i.|))" by Th16
      .= (g |^ |.i.| * (h |^ |.j.|))" by A1,Lm10
      .= h |^ j * (g |^ i) by A6,Th16;
  end;
end;

theorem
  g * h = h * g implies g * (h |^ i) = h |^ i * g
proof
  assume
A1: g * h = h * g;
  thus g * (h |^ i) = g |^ 1 * (h |^ i) by Th25
    .= h |^ i * (g |^ 1) by A1,Th38
    .= h |^ i * g by Th25;
end;

definition
  let G,h;
  attr h is being_of_order_0 means

  h |^ n = 1_G implies n = 0;
end;

registration
  let G;
  cluster 1_G -> non being_of_order_0;
  coherence
  proof
    (1_G) |^ 8 = 1_G by Lm4;
    hence thesis;
  end;
end;

definition
  let G,h;
  func ord h -> Element of NAT means
  :Def11:
  it = 0 if h is being_of_order_0
  otherwise
  h |^ it = 1_G & it <> 0 & for m st h |^ m = 1_G & m <> 0 holds it <= m;
  existence
  proof
    defpred P[Nat] means h |^ $1 = 1_G & $1 <> 0;
    thus h is being_of_order_0 implies ex n being Element of NAT st n=0;
    hereby
      assume not h is being_of_order_0;
      then
A1:   ex n being Nat st P[n];
      consider k being Nat such that
A2:   P[k] and
A3:   for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A1);
      reconsider k as Element of NAT by ORDINAL1:def 12;
      take k;
      thus h |^ k = 1_G & k <> 0 by A2;
      let m;
      assume h |^ m = 1_G & m <> 0;
      hence k <= m by A3;
    end;
  end;
  uniqueness
  proof
    let n1,n2 be Element of NAT;
    thus h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2;
    assume that
    not h is being_of_order_0 and
A4: h |^ n1 = 1_G & n1 <> 0 & ( for m st h |^ m = 1_G & m <> 0 holds
n1 <= m )& h |^ n2 = 1_G &( n2 <> 0 & for m st h |^ m = 1_G & m <> 0 holds n2
    <= m );
    n1 <= n2 & n2 <= n1 by A4;
    hence thesis by XXREAL_0:1;
  end;
  correctness;
end;

theorem Th40:
  h |^ ord h = 1_G
proof
  per cases;
  suppose
    h is being_of_order_0;
    then ord h = 0 by Def11;
    hence thesis by Def7;
  end;
  suppose
    h is not being_of_order_0;
    hence thesis by Def11;
  end;
end;

theorem
  ord 1_G = 1
proof
A1: for n st (1_G) |^ n = 1_G & n <> 0 holds 1 <= n by NAT_1:14;
  ( not 1_G is being_of_order_0)& (1_G) |^ 1 = 1_G by Lm4;
  hence thesis by A1,Def11;
end;

theorem
  ord h = 1 implies h = 1_G
proof
  assume
A1: ord h = 1;
  then not h is being_of_order_0 by Def11;
  then h |^ 1 = 1_G by A1,Def11;
  hence thesis by Th25;
end;

theorem
  h |^ n = 1_G implies ord h divides n
proof
  defpred P[Nat] means h |^ $1 = 1_G implies ord h divides $1;
A1: for n being Nat st for k being Nat st k < n holds P[k] holds P[n]
  proof
    let n be Nat;
    assume
A2: for k being Nat st k < n holds P[k];
    assume
A3: h |^ n = 1_G;
    per cases;
    suppose
      n = 0;
      hence thesis by NAT_D:6;
    end;
    suppose
A4:   n <> 0;
      per cases;
      suppose
        ord h = 0;
        then h is being_of_order_0 by Def11;
        hence thesis by A3,A4;
      end;
      suppose
A5:     ord h <> 0;
        then h is not being_of_order_0 by Def11;
        then ord h <= n by A3,A4,Def11;
        then consider m being Nat such that
A6:     n = ord h + m by NAT_1:10;
        h |^ n = h |^ ord h * (h |^ m) by A6,Lm5
          .= 1_G * (h |^ m) by Th40
          .= h |^ m by Def4;
        then ord h divides m by A2,A3,A5,A6,NAT_1:16;
        then consider i being Nat such that
A7:     m = ord h * i by NAT_D:def 3;
        n = ord h * (1 + i) by A6,A7;
        hence thesis by NAT_D:def 3;
      end;
    end;
  end;
  for n being Nat holds P[n] from NAT_1:sch 4(A1);
  hence thesis;
end;

definition
  let G be finite 1-sorted;

  redefine func card G -> Element of NAT;
  coherence
  proof
    card the carrier of G in NAT;
    hence thesis;
  end;
end;

theorem
  for G being non empty finite 1-sorted holds card G >= 1
proof
  let G be non empty finite 1-sorted;
  set g = the Element of G;
  {g} c= the carrier of G & card {g} = 1 by CARD_1:30,ZFMISC_1:31;
  hence thesis by NAT_1:43;
end;

definition

  let IT be multMagma;
  attr IT is commutative means
  :Def12:
  for x, y being Element of IT holds x*y = y*x;
end;

registration
  cluster strict commutative for Group;
  existence
  proof
    reconsider G0 = multMagma (# REAL, addreal #) as Group by Th3;
    take G0;
    thus G0 is strict;
    let a,g be Element of G0;
    reconsider A = a, B = g as Real;
    thus a * g = B + A by BINOP_2:def 9
      .= g * a by BINOP_2:def 9;
  end;
end;

definition
  let FS be commutative non empty multMagma;
  let x,y be Element of FS;
  redefine func x*y;
  commutativity by Def12;
end;

theorem
  multMagma (# REAL, addreal #) is commutative Group
proof
  reconsider G = multMagma (# REAL, addreal #) as Group by Th3;
  G is commutative
  proof
    let h,g be Element of G;
    reconsider A = h, B = g as Real;
    thus h * g = B + A by BINOP_2:def 9
      .= g * h by BINOP_2:def 9;
  end;
  hence thesis;
end;

reserve A for commutative Group;
reserve a,b for Element of A;

theorem
  (a * b)" = a" * b" by Th16;

theorem
  (a * b) |^ i = a |^ i * (b |^ i) by Th37;

theorem
  addLoopStr (# the carrier of A, the multF of A, 1_A #) is Abelian
  add-associative right_zeroed right_complementable
proof
  set G = addLoopStr (# the carrier of A, the multF of A, 1_A #);
  thus G is Abelian
  proof
    let a,b be Element of G;
    reconsider x = a, y = b as Element of A;
A1: for a,b be Element of G, x,y be Element of A st a = x & b = y holds a
    + b = x * y;
    thus a + b = x * y .= b + a by A1;
  end;
  hereby
    let a,b,c be Element of G;
    reconsider x = a, y = b, z = c as Element of A;
    thus a + b + c = x * y * z .= x * (y * z) by Def3
      .= a + (b + c);
  end;
  hereby
    let a be Element of G;
    reconsider x = a as Element of A;
    thus a + 0.G = x * 1_A .= a by Def4;
  end;
  let a be Element of G;
  reconsider x = a as Element of A;
  reconsider b = inverse_op(A).x as Element of G;
  take b;
  thus a + b = x * x" by Def6
    .= 0.G by Def5;
end;

begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.

theorem Th49:
  for L be unital non empty multMagma for x be Element of L holds
  (power L).(x,1) = x
proof
  let L be unital non empty multMagma;
  let x be Element of L;
  0+1 = 1;
  hence (power L).(x,1) = (power L).(x,0) * x by Def7
    .= 1_L * x by Def7
    .= x by Def4;
end;

theorem
  for L be unital non empty multMagma for x be Element of L holds (power
  L).(x,2) = x*x
proof
  let L be unital non empty multMagma;
  let x be Element of L;
  1+1 = 2;
  hence (power L).(x,2) = (power L).(x,1) * x by Def7
    .= x * x by Th49;
end;

theorem
  for L be associative commutative unital non empty multMagma for x,y be
Element of L for n be Nat holds (power L).(x*y,n) = (power L).(x,n)
  * (power L).(y,n)
proof
  let L be associative commutative unital non empty multMagma;
  let x,y be Element of L;
  defpred P[Nat] means
   (power L).(x*y,$1) = (power L).(x,$1) * (power L).(y,$1);
A1: now
    let n be Nat;
    assume P[n];
    then (power L).(x*y,n+1) = (power L).(x,n) * (power L).(y,n) * (x*y) by
Def7
      .= (power L).(x,n) * ((power L).(y,n) * (x*y)) by Def3
      .= (power L).(x,n) * (x*((power L).(y,n)*y)) by Def3
      .= (power L).(x,n) * (x*(power L).(y,n+1)) by Def7
      .= (power L).(x,n)*x * (power L).(y,n+1) by Def3
      .= (power L).(x,n+1) * (power L).(y,n+1) by Def7;
    hence P[n+1];
  end;
  (power L).(x*y,0) = 1_L by Def7
    .= 1_L * 1_L by Def4
    .= (power L).(x,0) * 1_L by Def7
    .= (power L).(x,0) * (power L).(y,0) by Def7;
  then
A2: P[0];
  thus for n be Nat holds P[n] from NAT_1:sch 2(A2,A1);
end;

:: Moved from ENDALG, 17.01_2006, AK

definition
  let G,H be multMagma;
  let IT be Function of G,H;
  attr IT is unity-preserving means
  IT.1_G = 1_H;
end;

subset_name: curated


TITLE: Is every infinite decimal sequence convergent?
QUESTION [3 upvotes]: Is every infinite decimal sequence convergent?
For example, would this sequence $x= 0.12112211122211112222\ldots$ be considered convergent?

REPLY [3 votes]: Yes, so long as there are only finitely many terms prior to the decimal. For any given number $n\in (0,1)$ with digits $a_i$ to the right of the decimal you can write it as:
$$n=\sum_{i=1}^\infty \frac{a_i}{10^i},$$
which converges absolutely, since $n\leq \sum_{i=0}^\infty 10^{-i}=10/9$.


TITLE: Is it good to use mean value theorem in $\epsilon-\delta$ continuity proofs?
QUESTION [6 upvotes]: I wanted to prove $f(x) = \cos(x)$ is continuous using $\epsilon-\delta$ proof
Couple of posts on MSE appealed to MVT to resolve this problem.
Namely:

$\exists c \in [x,x_o]$ s.t. $|\cos(x)-\cos(x_o)| = |\sin(c)||x-x_o|$

Tada!
Problem here is that we are appealing to the fact $\sin(x)$ is the derivative of $\cos(x)$
...which necessarily implies that $\cos(x)$ is continuous.
Is it "good" to use MVT in proving a function is continuous?

REPLY [1 votes]: The answer to the headline question is "No."  As the OP has asserted, the MVT assumes conditions stronger than continuity.  And its use is "circular logic."
I thought it would be instructive to present a $\delta-\epsilon$ proof.
To that end, here is a ...
HINT:
Use the Prosthaphaeresis Formula
$$|\cos(x)-\cos(x_0)|=2\left|\sin\left(\frac{x+x_0}{2}\right)\,\sin\left(\frac{x-x_0}{2}\right)\right| \tag 1$$
Along with the inequality
$$|\sin(x)|\le x \tag 2$$

SPOILER ALERT Scroll over the highlighted area to reveal the solution

Starting from $(1)$ and using $(2)$ along with $|\sin(x)|\le 1$ reveals $$|\cos(x)-\cos(x_0)|\le |x-x_0|$$Therefore, given $\epsilon>0$, then $$|\cos(x)-\cos(x_0)|<\epsilon$$whenever $|x-x_0|<\delta =\epsilon$.  And we are done!


TITLE: Projection map is closed or not?
QUESTION [4 upvotes]: If we consider projection of $\Bbb R\times \Bbb R$ onto the $x$-axis(codomain is $\Bbb R\times \Bbb R$) the map is not closed as we know the image of a hyperbola ($xy=1$, closed) is not closed.
In my functional analysis book
Theorem :
Let $X$ be a normed space and $P$ is a projection form $X$ to $X$. Then $P$ is closed map if and only if the subspaces Range $R(P)$ and Zero space $Z(P)$ are closed in X.
Definition of projection given is $P\circ P=P$.
the above example satisfies all the conditions in Theorem but the map is not closed.
please help me with this.

REPLY [5 votes]: The definition of a close map in Functional Analysis is different from the definition in general topology. In FA a linear map is closed iff its graph is closed, but in topology a map is closed iff it maps closed sets to closed sets.


TITLE: Conditional marginal distribution of conditional bivariate normal distribution
QUESTION [0 upvotes]: I have a bivariate normal distribution$$(X, Y)\sim N(\mu_{x}, \mu_{y}, \sigma_{x}^2, \sigma_{y}^2, \rho)$$ My question is : when $X > k$ ($k$ is a constant),how to get the distribution of $Y$?
Can anyone tell me how to solve it?
For exaple, let $$(X, Y) \sim N(0, 0, 1, 1, 0.7)$$
when $X > 1$, the distribution of $Y$?

REPLY [1 votes]: Using usual notation, the conditional (truncated) distribution $Y\mid X>k$ for some fixed $k$ is given by
\begin{align}
f_{Y\mid X>k}(y)&=\int_k^\infty\frac{f_{X,Y}(x,y)}{P(X>k)}\,dx
\\\\&=\frac{1}{P(X>k)}\int_k^\infty f_{Y\mid X=x}(y\mid x)f_X(x)\,dx\qquad,\,y\in\mathbb R
\end{align}
You can now find this density explicitly given any joint distribution $(X,Y)$.


TITLE: Using complex variables to find sums of Fourier series
QUESTION [2 upvotes]: Use complex variables to find the sum of the Fourier Series:
$$\sin(\theta) + \frac{\sin(2\theta)}{2^{2}} + \frac{\sin(3\theta)}{2^{3}}+\cdots$$
where $\theta$ is a real variable.

REPLY [3 votes]: We have
$$\begin{align}
f(\theta)&=\sin\theta + \sum_{k=2}^{\infty}\frac{\sin k\theta}{2^k} \tag 1\\\\
&=\sin\theta+\text{Im}\left( \sum_{k=2}^{\infty}\left(\frac{e^{i\theta}}{2}\right)^k\right) \tag 2\\\\
&=\sin\theta+\text{Im}\left(\frac{e^{i2\theta}}{2-e^{i\theta}}\right) \tag 3\\\\
&=\sin\theta+\frac12 \frac{2\sin 2 \theta-\sin \theta}{5-4\cos \theta} \tag 4\\\\
&=\frac12 \frac{9 \sin \theta-2\sin 2\theta}{5-4\cos \theta}\tag 5
\end{align}$$
In going from $(1)$ to $(2)$, we note that the imaginary part of $e^{i\theta}=\cos \theta+i\sin \theta$ is $\sin \theta$ and thus write $\sin \theta=\text{Im}(e^{ \theta})$.  We also make use of the fact that $e^{ik\theta}=\left(e^{i\theta}\right)^k$.
In going from $(2)$ to $(3)$, we made use of the sum for a geometric series $\sum_{k=m}^{\infty}r^k=\frac{r^m}{1-r}$ with $r=\frac{e^{i\theta}}{2}$.
In going from $(3)$ to $(4)$, we multiplied both numerator and denominator by the complex conjugate of the denominator, thereby rendering the denominator real and equal to the square of the magnitude of $2-e^{i\theta}$.

NOTE:
We remark that if the first term of the series were $\frac{\sin \theta}{2}$ rather than $\sin \theta$, then $(5)$ would be
$$\begin{align}
\frac12 \frac{9 \sin \theta-2\sin 2\theta}{5-4\cos \theta}-\frac 12 \sin \theta &=\frac12 \frac{9\sin \theta-2\sin 2 \theta-(5\sin \theta -2 \sin 2\theta)}{5-4\cos \theta}\\\\
&=\frac{2\sin \theta}{5-4\cos \theta}
\end{align}$$


TITLE: Show that there exists a prime ideal contained in $J = \{a \in R : ab = 0 \text{ for some } b\neq 0\}$
QUESTION [1 upvotes]: Let $R$ be a commutative ring with unity. Let
$$J = \{a \in R : ab = 0 \text{ for some } b\neq 0\}$$
Show that there exists a prime ideal contained in $J$.
Attempt:
I can see that this set contains all zero divisors along with zero itself.
Considering the contrapositive of the definition of prime ideal we need to prove that if $x,y \in J^c \implies xy \in J^c$.
Proof: Assume if possible $xy \in J$ then there exists a non-zero element $z$ such that $(xy)z = 0$, using the associative property of multiplication $x(yz) = 0$, now $yz \neq 0$ as $y \in J^c$ hence we can conclude $x(yz) \neq 0$. Which gives us the required contradiction.
There are two questions I want to ask:
Does the proof furnished above answer the question asked ?
But what I don't understand is why is the phrase "there exists a prime ideal contained in J" being used, why not use show that "J is the prime ideal"?

REPLY [2 votes]: That is because the set of zero-divisors, in general, is not even an ideal.
Counter-example: in $\mathbf Z/6\mathbf Z$ the zero-divisors are the congruence classes of $2, 3, 4$. These are not an ideal, since $2+3=5$, for instance, is a unit in $\mathbf Z/6\mathbf Z$.
Hint:
Consider the set of ideals contained in $J$, ordered by inclusion, and apply Zorn's lemma to obtain an ideal contained in $J$ which is maximal w.r.t. inclusion. Then show this ideal is prime .


TITLE: Matlab + Ordinary Least Squares (OLS) method
QUESTION [0 upvotes]: I'll be very grateful if you'll help me to solve the equation with Ordinary Least Squares (OLS) method + Matlab.

Given:
$P=\frac{mt}{b+t}$

Also:
t=[1,3,4,7,8,10]
P=[2.1, 4.6, 5.4, 6.1, 6.4, 6.6]
1) Write P in Matlab.

2) Find b,m by solving the equation with Ordinary Least Squares (OLS) method.

Thank's.

REPLY [1 votes]: Hint:
Write the equation this way
$$\frac{1}{P}=\frac{b}{m}\cdot\frac{1}{t}+\frac{1}{m}$$


TITLE: Prove derivative is continuous - is this $\delta/\epsilon$ proof correct?
QUESTION [3 upvotes]: I am aware of proofs of this fact, including those given at prove that $f'(a)=\lim_{x\rightarrow a}f'(x)$.. This question is not about how to prove it efficiently using MVT or any other clever method, but whether the proof I've sketched here is correct. This is not a duplicate, because I'm trying to get a review of my delta-epsilon reasoning.

Suppose $f$ is differentiable on an open interval $I$, $c\in I$, and $\lim_{x\to c} f'(x) = L \neq\infty$. Prove that $f'$ is continuous at $c$.

In other words, $f'$ cannot have a removable discontinuity. My intuition is this: if $x$ is close to $c$, then the quantity $\frac{f(x)-f(c)}{x-c}$ is close to $f'(x)$ and also to $f'(c)$, therefore they are close to each other. However, I'm having a hard time formalizing this.
I figure that for any $\epsilon >0$, we can find a $\delta$ so that, whenever $x$ is $\delta$-close to $c$, that puts our difference quotient $\frac{\epsilon}{2}$-close to $f'(c)$. That's true because $f'(c)$ exists.
Additionally, I can find another $\delta$ so that $f'(x)$ is $\frac{\epsilon}{2}$-close to $L$ when $x$ is $\delta$-close to $c$. That's true because the limit of $f'$ exists at $c$.
Choosing the smaller of the two $\delta$'s, the triangle inequality gives us that $|f'(c)-L|<\epsilon$, and so they're equal? Does that work?

REPLY [2 votes]: On OP's request I convert my comments into an answer.

While the argument put forth by OP in his question is almost correct, it needs to be substantiated by some amount of rigor. And precisely that is the reason it can't be considered as a correct proof.
Note that since $$\lim_{x\to c} \frac{f(x) - f(c)} {x-c} =f'(c) $$ it is correct to say that the difference quotient $(f(x) - f(c)) /(x-c) $ is near $f'(c) $ when $x$ is near $c$. And by interchanging the roles of $x$ and $c$ OP reasons that the quotient is also near $f'(x) $. This is a fundamental flaw but subtle to detect. The amount of closeness between $x$ and $c$ which is needed to ensure the closeness of the difference quotient to the value $f'(c) $ is not necessarily the same as that needed for making the difference quotient close to $f'(x)$. This is difficult to justify rigorously and ultimately it requires some sort of continuity of derivative at $c$ and this is what we actually need to prove.
The simplest approach is to use the mean value theorem and one of the answers has already given this approach. I will also use the same approach bu use the $\epsilon, \delta$ gymnastics. We are supposed to prove that $$\lim_{x\to c} \frac{f(x) - f(c)} {x-c} =f'(c) =L=\lim_{x\to c} f'(x)\tag{1} $$ where first and last equalities are given in the question and the middle one is to be established on the basis of those.
One of the techniques commonly used in analysis to establish the equality of two real numbers is to show that their difference is less than any arbitrarily given positive real number. So let $\epsilon>0$ be arbitrary and we will show that $|L-f'(c) |<\epsilon$. From the first equality in $(1)$ we know that there is a number $\delta_{1}>0$ such that $$\left|\frac{f(x) - f(c)} {x-c} - f'(c) \right|<\frac{\epsilon} {2}\tag{2}$$ whenever $0<|x-c|<\delta_{1}$. And similarly there is a number $\delta_{2}>0$ such that $$|f'(x) - L|<\frac{\epsilon} {2} \tag{3}$$ whenever $0<|x-c|<\delta_{2}$.
Let $\delta=\min(\delta_{1},\delta_{2})$ and let $x$ be any value satisfying $0<|x-c|<\delta$. Clearly the inequality $(2)$ holds for this value of $x$. By mean value theorem we see that there is a number $y $ between $x$ and $c$ such that $$\frac{f(x) - f(c)} {x-c} =f'(y) $$ and then the inequality  $(2)$ becomes $|f'(y) - f'(c) |<\epsilon/2$. Since $y$ lies between  $x$ and $c$ we have $$0<|y-c|<|x-c|<\delta\leq \delta_{2}$$ From inequality $(3)$ it now follows that $|f'(y) - L|<\epsilon /2$. We can now see via triangle inequality that $$|L-f'(c)|\leq |L-f'(y) |+|f'(y) - f'(c) |<\frac{\epsilon} {2}+\frac{\epsilon}{2}=\epsilon$$ and our proof is complete.


TITLE: combinatorial formula closed form
QUESTION [1 upvotes]: I have the following sum and I am struggling to show that the closed form is given by the R.H.S of (1).
$$
\sum^\tau _{j=1} \frac{(1-x)^{j-1}x}{1-(1-x)^\tau}(1-(1-x)^j) = \frac{1-(1-x)^{\tau+1}}{2-x} \tag 1
$$
Any help is appreciated as I am quite lost!

REPLY [1 votes]: The factor $\dfrac x {1-(1-x)^\tau}$ does not change as $j$ goes from $1$ to $\tau.$ Therefore by the distributive law, it can be pulled out of the sum:
$$
\sum^\tau _{j=1} \frac{(1-x)^{j-1}x}{1-(1-x)^\tau}(1-(1-x)^j) = \frac x {1-(1-x)^\tau} \sum_{j=1}^\tau (1-x)^{j-1} \Big(1-(1-x)^j)\Big).
$$
Next one can apply the distributive law one more time:
$$
\frac x {1-(1-x)^\tau} \sum_{j=1}^\tau (1-x)^{j-1} \Big(1-(1-x)^j)\Big) = \frac x {1-(1-x)^\tau} \sum_{j=1}^\tau\Big( (1-x)^{j-1} - (1-x)^{2j-1} \Big).
$$
This becomes two separate series:
$$
\frac 1 {1-(1-x)^\tau} \left( \sum_{j=1}^\tau (1-x)^j - \sum_{j=1}^n (1-x)^{2j-1} \right).
$$
Each of these is a finite geometric series and can be treated accordingly.


TITLE: Yet another combinatoric problem
QUESTION [0 upvotes]: we have the following question for homework:
N of the knights of the round table are having dinner.
In how many ways can they sit around the table?
What if Jack won't sit next to John and the queen -
how many possible ways exist now?

The first question for quite easy - (n-1)!. I'm struggling with the second one:
If Jack refuses to sit next to one of them I can count them as one, calculate and then subtract it from the total number of permutations. Its a little harder when he refuses
to sit next to two people, because they CAN sit next to each other.
Also, how can I think of it in term of equivalence classes? I am trying to adopt this way of thinking so a hint in that direction would be nice.
Thanks in advance!

REPLY [0 votes]: In the first part of the problem, it says N of the knights are having dinner.  Given there are M total knights, and K = M+1 chairs at the table (one extra for the queen).  This problem becomes, how many ways can you select N+1 seats from K total seats (combination) X how many ways you can arrange N knights and 1 queen (permutation).
This is C(K,N+1) x (N+1)! => (K!/((N+1)!x(K-N-1)!)) x (N+1)!  The (N+1)! term cancels out, giving: K! / (K-N-1)!
The second part's result is a subset of the first, so let J = K! / (K-N-1)!
The number of ways 3 people can be arranged (permutation) is 3!.  The number of ways to pick 3 contiguous seats from K chairs is K.  Therefore, the number of ways to seat 3 people contiguously in K chairs is K x 3!
Therefore:  J-(K x 3!) = (K! / (K-N-1)!) - (K x 3!)


TITLE: Topological Vector Space not induced by Metric
QUESTION [2 upvotes]: Can anyone give me an example of a Topological Vector Space that is not metrizable? I know that the neighborhood base of $0$ needs to be incountable, and all I can construct then is no topological vector space because the algebraic operations (especially multiplication) aren't continous.

REPLY [2 votes]: Take for instance $\mathbb{R}^{\mathbb{R}}$ with the product topology or the weak topology on an infinite-dimensional Banach space. You will find more examples here.


TITLE: relation between solution of a linear program and its perturbation
QUESTION [5 upvotes]: I have a linear program over a finite set of points $(x_1, x_2,\ldots, x_m)\in\mathbb{R}^n$:
$$
\max_j c' x_j
$$
Suppose the solution of this LP is obtained at a point $x_{j_1}$, which is a vertex of the convex polytope generated by these points.
Now, I perturb the linear function $c$ to $d$ such that $\lVert c -d\rVert_2 < \delta$, and perturb each point to $(y_1,y_2,\ldots,y_m)\in\mathbb{R}^n$ such that $\lVert x_j - y_j\rVert_2 < \epsilon$, and get the following perturbed linear program:
$$
\max_j d' y_j
$$
Suppose the solution of this perturbed LP is obtained at a point $y_{j_2}$. Are there any known upper bounds on $\lVert x_{j_1} - y_{j_2}\rVert_2$?

REPLY [1 votes]: I think that Igor refers to "smoothed analysis", which has been invented by Spielman and Teng to explain the performance of the simplex method. However, their result does not make a statement about how the optimal solution changes by the perturbation. Furthermore, for their result - a polynomial upper bound for the running-time of simplex, where the randomness is over the perturbation - it is crucial that the matrix describing the linear constraints is perturbed.
Without any further information about the polytope and how the objective function is perturbed (e.g., randomly or deterministically), it seems to be impossible to say anything useful - see Noah's comment, for instance.