TITLE: Supremum of Banach Spaces
QUESTION [12 upvotes]: Let $X$ be a linear space with a family of complete norms $(\| \circ \|_I)_{I \in \mathcal{I}}$ on $X$, i.e. for every $I \in \mathcal{I}$ the tuple $(X,\|\circ\|_I)$ is a Banach space. Now define $$\| x \|_\infty := \sup_{I \in \mathcal{I}} \| x \|_I \in [0,\infty]$$ for every $x \in X$ and $X_\infty = \{ x \in X ~:~ \|x\|_\infty < \infty \}$. It is easy to see that $(X_\infty,\|\circ\|_\infty)$ is a normed space. In particular, $X_\infty$ is a linear space.
Is $(X_\infty,\|\circ\|_\infty)$ a Banach space, i.e. is it complete?
My guess would be negative, but I can't come up with an (counter-)example.
What I have tried so far: It is easy to see that if $X$ is finite-dimensional and $\mathcal{I}$ is finite, then $(X_\infty,\|\circ\|_\infty)$ is again complete. Therefore I asumme that either I have to find many "incompatible" norms on a finite-dimensional space, or only "a few" norms on a "complicated" space. I would appreciate hints for either direction.

REPLY [4 votes]: The answer is no.
If $I$ is finite, then $X_\infty=X$ as linear spaces, so I assume $I$ is finite. Using open mapping theorem one can show that if $(X_\infty,\Vert\cdot\Vert_\infty)$ is Banach space then all the spaces $(X_\infty,\Vert\cdot\Vert_i)$ are isomorphic. Indeed, for all $i\in I$ the map
$$
\mathrm{Id}:(X_\infty,\Vert\cdot\Vert_\infty)\to(X_\infty,\Vert\cdot\Vert_i):x\mapsto x
$$
is bounded and bijective, hence isomorphism. Since for all $i\in I$ we have $(X_\infty,\Vert\cdot\Vert_\infty)\cong(X_\infty,\Vert\cdot\Vert_i)$, the spaces $(X_\infty,\Vert\cdot\Vert_i)$ for $i\in I$ are pairwise isomorphic.
Now to construct a counterexample it is sufficient to introduce finitely many non-isomorphic Banach space structures on the same linear space $X$. I'll construct two structures.
Let $(X,\Vert\cdot\Vert)$ be a separable Banach space non-isomorphic to $\ell_2$. For example take $X=(\ell_p,\Vert\cdot\Vert_p)$ with $p\neq 2$. Now consider norm $\Vert\cdot\Vert'$ given in this answer which turns $X$ into a Hilbert space. By construction $(X,\Vert\cdot\Vert)$ and $(X,\Vert\cdot\Vert')$ are not isomorphic. So norms $\Vert\cdot\Vert$ and $\Vert\cdot\Vert'$ gives the desired counterexample.


TITLE: Finite abelian group whose automorphism group is some general linear group
QUESTION [5 upvotes]: Let $G$ be a finite abelian group such that for some integer $n>1$, we have $\operatorname{Aut}(G) \cong \operatorname{GL}(n, \mathbb Z/2\mathbb Z )$. Is it true that $G\cong (\mathbb Z/2\mathbb Z )^n$ ?

REPLY [3 votes]: Let me write down a couple of thoughts (not yet a proper answer) and I'll get back to this problem a little later, as I have to leave now.
First, the automorphism group of a $p$-group is never trivial unless the group has order $2$.
Second, since an abelian group is the direct product of its Sylow subgroups, and since automorphism groups behave well with respect to direct products of groups of coprime orders, it follows that the automorphism group of an abelian group is the direct product of the automorphism groups of its Sylow subgroups.
Third, no general linear group is directly decomposable, i.e. you can't write a general linear group as a direct product of proper subgroups.
So if there is a minimal counterexample, then it must be a $p$-group.
At this point, you need to know how to find the order (but perhaps not necessarily the structure) of the automorphism group of an abelian $p$-group.
This is given by Theorem 4.1 of this paper.
Assuming that $G = C_{p^{e_1}} \times \ldots \times C_{p^{e_r}}$, where $e_1 \leq \ldots \leq e_r$, we have
$$\lvert \operatorname{Aut}(G) \rvert = \prod_{k=1}^r(p^{d_k}-p^{k-1})\prod_{j=1}^r p^{e_j(r-d_j)}\prod_{i=1}^r p^{(e_i-1)(r-c_i+1)},$$
where $d_k = \operatorname{max}\{s:e_s=e_k\}$ and $c_k = \operatorname{min}\{s:e_s=e_k\}$, for $1 \leq k \leq r$.
We are also assuming that $\lvert \operatorname{Aut}(G) \rvert = \lvert \operatorname{GL}_n(2) \rvert$ for some positive integer $n>1$. Thus the problem essentially reduces to showing that if
$$\lvert \operatorname{Aut}(G) \rvert = \prod_{k=1}^r(p^{d_k}-p^{k-1})\prod_{j=1}^r p^{e_j(r-d_j)}\prod_{i=1}^r p^{(e_i-1)(r-c_i+1)} =  \lvert \operatorname{GL}_n(2) \rvert = 2^{\frac{n(n-1)}{2}}\prod_{i=1}^n (2^i-1),$$
then $p =2$, $n=r$ and $e_1 = \ldots = e_r=1$.
Let $$p^A =\prod_{j=1}^r p^{e_j(r-d_j)}\prod_{i=1}^r p^{(e_i-1)(r-c_i+1)}.$$
Then $$p^Ap^{\frac{r(r-1)}{2}}\prod_{k=1}^r(p^{d_k-(k-1)}-1) = 2^{\frac{n(n-1)}{2}}\prod_{i=1}^n (2^i-1).$$
By using the result cited by Dietrich Burde, we can assume that $p>2$.
Then $2^{\frac{n(n-1)}{2}}$ must divide the quantity $\prod_{k=1}^r(p^{d_k-(k-1)}-1)$. I'll pick this up tomorrow.

I am not sure that this approach leads anywhere. Meanwhile, I have mentioned this problem to Marty Isaacs and he destroyed it effortlessly. Here's his solution:
Suppose that $G$ is finite abelian but not an elementary abelian $2$-group and such that $\operatorname{Aut}(G) \cong \operatorname{GL}_n(2)$, $n>1$. The map $g \to g^{-1}$ is an automorphism of $G$, has order $2$ (since $G$ is not an elementary abelian $2$-group) and lies in the centre of $\operatorname{Aut}(G)$ (check this). But $\operatorname{GL}_n(2)$ has trivial centre, contradiction. Thus $G$ is an elementary abelian $2$-group and since the sequence $\lvert \operatorname{GL}_n(2) \rvert$ is strictly increasing in $n$, we get $|G| = 2^n$ thus $G \cong C_2^n$.


TITLE: Finding final equilibrium temperature?
QUESTION [0 upvotes]: "A 100g mass is heated with a strong flame for 10 seconds then placed into a crucible on a heat proof mat. After cooling for 5 minutes the 100g mass is at 67.6C while the table it's resting on is at 24.2C. What will be the final temperature of the mass?"
Our teacher assigned us this problem to work on and its one I don't think is possible to solve without some extra information such as the heat capacities of both of the masses.
I tried adding both temps together and divided them to get the final temperature/average but I don't think that approach was going to be accurate. It takes different amounts of joules to increase the temperature of dissimilar materials, meaning if one loses a certain amount of joules the other will increase in temp but not by the same amount as the other substance(correct me if I'm wrong).
This is why I think the problem might need more information but when confronting my teacher with this she just said this in reply "Basically, the final temp of the mass will end up being the same temperature of the room. It will heat the room by a tiny, tiny, tiny quantity, but essentially end up at room temp."
Am I missing something here? This is my first thermodynamics orientated class so I'm not well versed. Thank you in advance.
Edit: here is the other information we are given:
The initial temp is 25.9C and the sample was at 180.2C after being heat up. The flame temp 190.5C. Conduction, convection, radiation are all involved.

REPLY [0 votes]: the crucial information is "After cooling for 5 minutes the 100g mass is at 67.6C while the table it's resting on is at 24.2C"
since the table did noch change temperature in the first 5 minutes, why should it with smaller temperature difference in the next time. So you have to read the question very carefully, to look for the answer. So your teacher was right.


TITLE: $h(x+y)+h(0)=h(x)+h(y)$ iff only if $h(x)$ is affine or constant
QUESTION [2 upvotes]: Let $h : \mathbb{R}^n \to \mathbb{R}^n$ satisfy
\begin{align}
h(x+y)+h(0)=h(x)+h(y).
\end{align}
Can we show that that the only functions that satisfy the above property are affine functions (i.e., $h(x)=Ax+b$) or constant functions.
Proof for $n=1$.
I have a proof for $n=1$ with an extra assumption of differentiability.
Take the derivative with respec to $x$
\begin{align}
\frac{d}{dx} h(x+y) = \frac{d}{dx}  h(x)
\end{align}
since, $y$ and $x$ are arbitrary this implies  $h(x)$ is either a constant or and affine function or constant functions.
It is not difficult to extend this proof to $n>1$. However, I am not satisfied with it as it assumes differentiability.
My question: Can we show the conjectured result without any differentiability assumptions? Also, I am not sure if continuity must be assumed. It would be nice to know if continuity is required or not.

REPLY [0 votes]: Let $g(x)=h(x)-h(0)$ so that $g(0)=0$. Then,
\begin{align}
      g(x+y) & =h(x+y)-h(0) \\
             & = h(x+y)+h(0)-2h(0) \\
             & = h(x)+h(y)-2h(0) \\
             & = g(x)+g(y).
\end{align}
Hence $0=g(0)=g(-x+x)=g(-x)+g(x)$, which gives
$$
     g(-x)=-g(x).
$$
The function $g$ is linear over the rational scalars, but not necessarily over all reals. By induction,
$$
          g(nx) = ng(x),\;\;\ n=0,1,2,\cdots,\;\; x\in\mathbb{R}^n.
$$
Therefore, if $q=\frac{m}{n}$ for integers $n,m$ with $n\ne 0$,
$$
            n g(qx) = g(nqx)=g(mx)=mg(x) \implies g(qx) = q g(x),\;\; q\in\mathbb{Q}.
$$
This is not enough to imply linearity of $g$, unless, for example, you assume $g$ is continuous. To see why this is so, it is enough to find a function $h$ on $\mathbb{R}$ that is additive, but not linear. The Axiom of Choice is needed to construct $h : \mathbb{R}\rightarrow\mathbb{R}$ such that $h(x+y)=h(x)+h(y)$ for all $x,y\in\mathbb{R}$, but which is not linear. Using what has been done so far, you can see that
$$
             h(\frac{m}{n}r) = \frac{m}{n}h(r),\;\;\; m,n\in\mathbb{Z}, n \ne 0, r\in\mathbb{R}.
$$
So $h$ is linear on $\{ qr : q \in \mathbb{Q} \}\subset\mathbb{R}$ with linear multiplier $h(r)$.
The problem is that you can have different multipliers on different sets of this type, $\{ qr : q \in\mathbb{Q} \}$. $\mathbb{Q}$ can be partitioned into disjoint subsets on which the $h$ must be linear. This is done by defining an equivalence relation on $\mathbb{R}\setminus\{0\}$ by $x \sim y$ iff $y/x \in \mathbb{Q}$ (or $x/y\in\mathbb{Q}$.) It's easy to check that this is an equivalence relation, meaning that it is reflexive, symmetric, and transitive. An equivalence class $[x]$ containing $x\in\mathbb{R}\setminus\{0\}$ has the form $[x]=\{ qx : q \in \mathbb{Q}, q\ne 0 \}$. The function $h$ is linear on $[x]$ with $h(qx)=qh(x)$, and this defines $h$ on $[x]$ because every $y\in [x]$ is a rational multiple of $x$. If $\{ [x_\alpha]\}_{\alpha\in\Lambda}$ are disjoint equivalence classes whose union is $\mathbb{R}\setminus\{0\}$, then $h$ is uniquely determined on $\mathbb{R}$ by the values of $h(x_\alpha)$, and these values may be assigned to be arbitrary real numbers. This describes all possible additive functions on $\mathbb{R}$. Such a function $h$ can be highly discontinuous, depending on the choice function $\alpha\mapsto h(x_\alpha)$. The different slopes are $m_{\alpha}=h(x_\alpha)/x_\alpha$. $h$ is continuous iff all these slopes $m_{\alpha}$ are the same. In fact, $h$ is Lebesgue measurable iff all the slopes are identical. This construction is intimately connected with the argument used to establish the existence of non-measurable subsets of $\mathbb{R}$, so much so that you show that there exists a discontinuous additive function $h$ on $\mathbb{R}$ iff there exists a non-measurable subset of $\mathbb{R}$; there are no such things without the Axiom of Choice.


text:
\begin{document}
\title[Period sets of linear toral endomorphisms on $\TT^2$]
{Period sets of linear toral endomorphisms on $\TT^2$}

\author[J. Llibre]{Jaume Llibre $^{1}$}
\address{$^{1,2}$Departament de Matem\`{a}tiques,
Universitat Aut\`{o}noma de Barcelona, 08193 Bellaterra, Barcelona,
Catalonia, Spain} \email{jllibre@mat.uab.cat}

\author[N. Neum\"arker]{Natascha Neum\"arker $^{1,2}$}
\address{$^{2}$Matem\'atick\'y \'ustav Slezsk\'e Univerzity v Opav\v{e},
74601 Opava, \v{C}esk\'a republika}
\email{natascha.neumarker@math.slu.cz}

\subjclass[2010]{Primary 54H20.}

\keywords{periodic points, period, toral endomorphisms,
$2$--dimensional torus maps}

\begin{abstract}
The period set of a dynamical system is defined as the subset of all
integers $n$ such that the system has a periodic orbit of length
$n$. Based on known results on the intersection of period sets of
torus maps within a homotopy class, we give a complete
classification of the period sets of (not necessarily invertible)
toral endomorphisms on the $2$--dimensional torus $\TT^2$.
\end{abstract}

\maketitle

\section{Introduction and statement of the main results}

The sets of periods that are present in a dynamical system is one of
the key quantities which characterises the system. For continuous
maps on the interval, the celebrated theorem by Sharkovsky provides
a complete characterisation of period sets in terms of the
Sharkovsky ordering. A generalisation of Sharkovsky's Theorem to the
circle was obtained by the authors  Block, Coppel, Guckenheimer,
Misiurewicz and Young \cite{B, BC, BGMY, Mi}, for a unified
proof see \cite{ALM}. For other classes of maps where the period sets
have been studied see for instance \cite{ALM2, H, K, Ll}.

\smallskip

Toral or torus endomorphisms are continuous mappings of the torus that preserve
its group structure,
hence in the additive notation $\TT^m \cong \RR^m/\ZZ^m$, they can be
represented as $m\times m$ integer matrices, see for instance
\cite[Chapter~0]{W}.
In the present article, the term `toral endomorphism' is always used in this
sense, that is, for a map on the torus which is induced by the action
of an integer matrix modulo 1.
They serve as a standard example in the theory of discrete dynamical
systems and ergodic theory, and particularly the case of hyperbolic
toral automorphisms,
corresponding to integer matrices with determinant $\pm 1$ and no eigenvalues
on the unit circle, has been studied extensively because of its
interesting dynamical properties, compare \cite{W,KH}.
In \cite{TP}, the period sets of toral automorphisms on $\TT^2$
were investigated.

\smallskip

Minimal period sets are the intersection of all period sets arising
from maps in the same homotopy class; the origins of their study go
back to Alsed\'a, Baldwin, Llibre, Swanson and Szlenk \cite{ABLSS},
see also \cite{JM, JL}. Associated with each homotopy class, one has
a unique integer matrix $A$, which defines the action on the first
homology group, and this integer matrix, in turn, defines an
endomorphism of the torus, $f^{}_A$, hence it is itself a member of the
homotopy class. An important result in arbitrary dimension is that
the minimal period set of a homology class ``essentially'' coincides
with the period set of the associated toral endomorphism, apart from
possibly those periods that may arise from roots of unity among the
eigenvalues of this matrix, see \cite{JL}. However, in many of the
cases in which $\pm 1$ is among the eigenvalues, one finds that the
minimal period set and the period set of the endomorphism totally
differ and it can be concluded that, in these cases, the
endomorphism is not a good model for the dynamics of its homotopy
class with respect to periodic orbits.

\smallskip

For circle maps, the situation is comparatively simple and is
displayed in Table~1. The period sets only depend on the
degree $d$ of the map, listed in the first column; the second and
the third column refer to the minimal period set and the period set
of the corresponding endomorphism, respectively; the last column
answers the question whether the endomorphism defining the class
under consideration is invertible, hence an automorphism.
Here, the linear endomorphism $f_A$ is given by $f^{}_{(d)}(x) = d\cdot x$.

\bigskip
\bigskip

\begin{center}
\begin{tabular}{|c|c|c|c|}
 d    &    $\MPer(f_A)$     & $\Per(f_A)$    &  $\in\mathrm{Aut(\TT)}$?
 \\\hline
 1    & $\emptyset$       & $\{1\}$    &   yes \\ \hline
 0    & $\{1\}$       & $\{1\}$        &  no \\ \hline
 -1   & $\{1\}$       & $\{1,2\}$      &  yes \\ \hline
 -2   & $\NN\setminus\{2\}$  & $\NN\setminus\{2\}$    &  no \\ \hline
 $d\in\ZZ\setminus \{-2,-1,0,1\}$   & $\NN$      & $\NN$      & no \\\hline
\end{tabular}
\end{center}
\begin{center}
{\bf Table 1. Period sets for circle maps.}
\end{center}

\bigskip

In this article, we compare the minimal period sets of maps on
$\TT^2$ with the period set of the associated toral endomorphism,
aiming for an analogue of the above table for dimension $2$.

\smallskip

To obtain a complete classification, a variety of partly very
different techniques is employed. The minimal period sets were
derived in \cite{ABLSS} by means of estimating Nielsen numbers, see
\cite{H} for background reading on this approach. The study of
period sets in the special case of toral automorphisms in \cite{TP}
is based on an extensive distinction of cases; we note that much of
the reasoning in \cite{TP} makes use of the assumption of a
determinant $\pm 1$ and hence does not directly generalise to
arbitrary $2\times 2$ matrices.
We complete the classification of period sets by making use of
results on \textit{local conjugacy}, that is conjugacy modulo $n$,
$n\in\NN$, which corresponds to the action of the matrix on the
invariant subsets of points with rational coordinates.

\smallskip

The outline of this article is as follows. In Section
\ref{S:knownStuff} we compile the theory of minimal period sets and
periods of toral endomorphisms as far as needed for our purpose,
derive the period sets $\Per(f_A)$ from the minimal period sets
$\MPer(f_A)$ wherever
possible and identify the cases that require individual treatment.
In Section \ref{S:completion}, we complete the classification of
period sets on the two-dimensional torus by considering normal forms
for matrices with an eigenvalue $\pm 1$.
At the end of this introductory section, we summarise the results of our
later analysis in form of a comprehensive table.

\smallskip

The following Table 2 constitutes the $2$--dimensional analogue of Table 1 for
circle maps. Starting from some $A\in\Mat(2,\ZZ)$, the columns (from
left to right order) refer to the eigenvalues of $A$, the pair of
the trace and the determinant of $A$, i.e. $(t,d)= (\tr(A),\det(A))$,
the minimal polynomial $\mu_A^{}$, the minimal period
set $\MPer(f_A)$ of the homotopy class of $f_A$, the period set
$\Per(f_A)$, and finally an answer to the question whether
$f_A\in\End(\TT^2)$ is invertible, hence an element of
$\textrm{Aut}(\TT^2)\subset\End(\TT^2)$.
The symbol $\chi^{}_A$ denotes the characteristic polynomial of
the matrix $A$; the symbol $E$ refers to the set of exceptional integer
values $E= \{-2,-1,0,1\}$.

\bigskip
\bigskip

\input{summaryTable2D}

\bigskip

\begin{center}
{\bf Table 2. Period sets for torus maps.}
\end{center}

\section{Definitions and overview of results}\label{S:knownStuff}

The set of periods of a map $f:\TT^m\rightarrow\TT^m$ will be
denoted by
\[
\Per(f) \coloneqq \{n\in\NN \mid f\ \text{has an orbit of length}\
n\}.
\]
The \emph{minimal} set of periods is defined as
the intersection of all period sets in a given homotopy class,
\begin{equation}\label{E:IntersectionMPer}
\MPer(f_A) \coloneqq \bigcap_{g\simeq f} \Per(g),
\end{equation}
where $g\simeq f$ means that $g$ is homotopic to $f$.

Associated with a torus map $f:\TT^m \rightarrow \TT^m$, one has the
first induced homology map $f_{*1}:H_1(\TT^m,\ZZ) \rightarrow
H_1(\TT^m,\ZZ)$, which corresponds to some $m\times m$ integer
matrix $A$. In the following, we will denote by $\Mat(m,R)$ the ring
of $m\times m$ matrices with entries from the ring $R$. By
$\Mat(m,R)^{\times}$ we will refer to the invertible matrices over $R$
or, equivalently, to those elements of $\Mat(m,R)$ whose determinant
is a unit in $R$.
The linear map defined by the matrix $A : \RR^m\rightarrow
\RR^m$, covers a unique torus endomorphism
$f_A:\TT^m\rightarrow\TT^m$ whose action is given by matrix
multiplication modulo $1$, that is, two points $x,y\in\RR^m$ cover
the same element of $\TT^m$ if and only if $x-y\in\ZZ^m$. By
$\End(\TT^m)$ we denote the set of toral endomorphisms, and by
$f_A\in\End(\TT^m)$ we refer to the map induced by
$A\in\Mat(m,\ZZ)$. As $f_A \simeq f$, the intersection on the
right-hand side of Equation \eqref{E:IntersectionMPer} comprises the
period set of $f_A$, so one always has $\MPer(f_A)\subset
\Per(f_A)$. In fact, these two sets are typically more closely
related; in \cite[Proposition~3.4]{ABLSS} the following general
result is proved
\begin{equation}\label{E:MPerPerOfEndo}
   \MPer(f) = \Per(f_A)\setminus\{k\in\NN : 1\
   \text{is an eigenvalue of $A^n$}\}.
\end{equation}

In other words, the period set of the endomorphism $f_A$ and the
minimal period set $\MPer(f)$ coincide if and only if $A$ does not
have any eigenvalues that are roots of unity. In this case, the
number of fixed points of $A^n$ can be calculated in terms of the
\emph{Nielsen numbers}: $f_A^n$ has $N(f_A^n)$ isolated fixed
points, where
\[
   N(f_A^n) = \abs{\det(\id - A^n)},
\]
and $\id$ denotes the $m\times m$ identity matrix.
For $m=2$, this simplifies to
\[
   N(f_A^n) = \abs{1+ \lambda_1^n\lambda_2^n -(\lambda_1^n+\lambda_2^n)},
\]
where $\lambda_1,\lambda_2$ are the eigenvalues of $A$.

\smallskip

When the matrix $A$ has an eigenvalue that is an $n$-th root of
unity, the Nielsen numbers vanish for all multiples of $n$. In this
case, $n$ is not in the minimal period set; however, the endomorphism
$f_A$ admits periodic points of period $n$, which form
subtori of $\TT^m$. A treatment of this case can be found in the
appendix of \cite{BHP}.

\smallskip

The rational points of $\TT^m$ form an invariant subset of $\TT^m$
and can be written as the countable union of the finite sets of
$n$-division points, $n\in\NN$,
\[
[0,1)^m \cap\QQ^m = \bigcup_{n\in\NN} \left\{\left(\frac{k_1}{n},
\ldots,\frac{k_m}{n}\right) \mid 0\leq k_1,\ldots, k_m < n\right\} =
\bigcup_{n\in\NN} L_n.
\]
Each rational lattice $L_n$ in the union on the right-hand side is
invariant under the action of the integer matrix $A$, hence $L_n$ is
partitioned into finite orbits by $f_A$. Denoting by $\PerP(f)$ the
periodic \emph{points} of a map $f$, we can state that, if
$\gcd(n,\det(A))=1$, $L_n \subset \PerP(f_A)$, hence
$$
\bigcup_{n\in\NN \, : \, \gcd(n,\det(A))=1} L_n \subset \PerP(f_A),
\quad \mbox{and} \quad  \bigcup_{n\in\NN} L_n \subset \PerP{(f_A)}
$$
if $\det(A)=\pm1$, that is, if $A$ is an automorphism. In the
absence of roots of unity among the eigenvalues, all periodic points
are isolated and live on the rational lattices, whence the converse
$\PerP(f_A) \subset \bigcup_{n\in\NN} L_n$ follows, and one has strict
equality if
$A$ is invertible, as all lattice points are then consumed in periodic
orbits.
There is an abundance of literature dealing with
the periods of toral endomorphisms (mostly restricted to the
invertible case, i.e. automorphisms) on the rational lattices $L_n$
depending on $n$; for an overview, see, for instance, the articles
\cite{PV, BF, BRW, BNR} and references therein.

The rational lattice $L_n$ can be identified with the free module
over the finite ring $\ZZ/n\ZZ$, so studying the action of an
integer matrix on $L_n$ amounts to studying the matrix action modulo
$n$, and the question whether two integer matrices share the same
orbit structure on $L_n$ is closely related to the question of
conjugacy over the residue class ring $\ZZ/n\ZZ$. Two matrices that
are conjugate over $\ZZ/n\ZZ$ necessarily exhibit the same orbit
structure on $L_n$.

\smallskip

On the two-dimensional torus, one can formulate a necessary and
sufficient criterion for matrices to be locally conjugate on a
lattice $L_n$ for some or all $n\in\NN$ in terms of trace,
determinant and a third invariant, which we now define.

\begin{defin}
The matrix gcd (short mgcd) of a matrix $M= \displaystyle
\left(\begin{matrix} \alpha & \beta\\\gamma & \delta\end{matrix}\right)$
$\in\Mat(2,\ZZ)$ is defined as $\mgcd(M) \coloneqq \gcd(\beta,\gamma,\delta-\alpha)$.
\end{defin}

We note that the square of $\mgcd(M)$ always divides the discriminant
$\Delta (M) = \tr(M)^2-4\det(M)$,
\begin{equation}\label{E:mgcdDivDiscr}
\Delta(M) = (\alpha+\delta)^2 - 4(\alpha \delta -\beta \gamma)
= (\alpha + \delta)^2 - 4 \beta \gamma.
\end{equation}
The following theorem asserts trace, determinant and mgcd to be a
complete set of invariants with respect to local conjugacy.

\begin{theorem}[{\cite[Theorem~2]{BRW}}]\label{T:mgcd}
For two integer matrices $M,M^{\prime}\in\Mat(2,\ZZ)$, the following
statements are equivalent.
\begin{itemize}
\item[(a)] The reductions mod $n$ of $M$ and $M^{\prime}$ are
$\Mat(2,\ZZ/n\ZZ)^{\times}$ conjugate.

\item[(b)] $M$ and $M^{\prime}$ share the same trace, determinant and
mgcd.
\end{itemize}
\end{theorem}

We will make use of this theorem in Section~\ref{S:completion} in
order to determine the period sets of certain toral endomorphisms
with integer eigenvalues. Now we first treat the cases of complex
and irrational real eigenvalues, for which the period sets of toral
endomorphisms can be gained from the minimal period sets of their
homotopy classes.

\subsection{Complex eigenvalues and finite orders}

If $\xi\in\CC\setminus\RR$ is the eigenvalue of a matrix
$A\in\Mat(2,\ZZ)$, its complex conjugate $\bar{\xi}$ is the second
eigenvalue of $A$ and the determinant $d = \xi\bar{\xi} =
\abs{\xi}^2$ is consequently a positive integer.

\smallskip

If $d=1$, both roots lie on the unit circle, that is, they have
modulus $1$ and they are actually roots of unity. (This is a special
case of a more general fact: if all algebraic conjugates of an
algebraic integer $\alpha$ have modulus $1$, $\alpha$ is a root of
unity.) But if all eigenvalues of the matrix $A$ are distinct roots
of unity, $A$ has finite order, that is, there is some integer $n$
such that $A^n = \id$.

\smallskip

It is well-known that for each $n$ the finite orders of subgroups of
$\GL(n,\ZZ)$ can only assume certain values, determined by all factors
of the cyclotomic polynomials that are elements of $\ZZ[x]$ and have
degree $n$, hence are the characteristic polynomial of a matrix
in $\GL(n,\ZZ)$.
Furthermore, for $2n$ and $2n+1$, the lists of possible
orders coincide, more specifically, $\GL(n,\ZZ)$ for $n=2$ and $3$
can have subgroups of the finite orders $1,2,3,4,6$, see \cite{KP},
for example.

\smallskip

For $2\times 2$ integer matrices, these cases correspond to the
characteristic polynomials $x^2+x+1$, $x^2+1$, $x^2-x+1$ whose roots
are $e^{2 i \pi/3},e^{-2 i \pi/3}$, $\pm i$ and $e^{i\pi/3},e^{-i\pi/3}$,
respectively. In \cite{TP} the periods of the corresponding
automorphisms are derived from the characteristic equations; using
the knowledge about the minimal period sets, one can treat these
three cases at once.
\textit{They are represented in rows 6--8 of Table~2}.

\begin{lemma}
   Assume $A\in\Mat(2,\ZZ)$ is of finite order $k=\ord(A)$.
   Then $k\in\Per(f_A)$.
   Consequently, for $A\in\Mat(2,\ZZ)$ whose eigenvalues are complex roots
   of unity, one finds $\Per(f_A) = \MPer(f_A)\cup\{\ord(A)\}$.
\end{lemma}
\begin{proof}
The fact that $A$ has order $k$ means $A^k - \id$ is the zero matrix
but for every $d<k$, $A^d-\id$ is not zero. But that means, there is
some $n\in\NN$ such that $A^d - \id \not\equiv 0 \mod n$ for every
$d<k$. Consequently, there is some $x = (\alpha,
\beta)\in(\ZZ/n\ZZ)^2$ such that $(A^d-\id)x \not= 0$ over
$\ZZ/n\ZZ$ for every $d<k$. Hence, the point $x$ has period $k$. The
last statement follows because the period set of a matrix of order
$k$ can contain divisors of $k$ only, and in the cases under
consideration, all divisors $d$ of $k$ with $d<k$ are already
contained in the set
$\MPer(f_A)\subset\Per(f_A)\subset\{d: d|k\}$.
\end{proof}

Note that the matrix order is absent from the set of minimal periods
of the homotopy class, as for $A^n=\id$, one has $N(f^{j\cdot
n}_A)=0$ for all $j\in\NN$. The cases of integer roots of unity will
be dealt with in Section \ref{S:completion}.

\smallskip

If the eigenvalues in $\CC\setminus\RR$ are not roots of unity, the
determinant has to be greater than $1$. The period sets of the
remaining cases with non-real eigenvalues are given by the following
theorem \cite[Thm.~4.24]{ABLSS}.

\begin{theorem}[\cite{ABLSS}]\label{CnoRU}
If $d\geq 2$ and $\lambda,\mu\in\CC\setminus\RR$ then
$\MPer(f_A)=\NN$, unless the pair $(t,d)$ is one of the following
cases:
\begin{itemize}
\item[(a)] If $(t,d)=(-2,2)$, then $\MPer(f_A) =\NN\setminus\{2,3\}$.

\item[(b)] If $(t,d)=(-1,2)$, then $\MPer(f_A) =\NN\setminus\{3\}$.

\item[(c)] If $(t,d)=(0,2)$, then $\MPer(f_A) =\NN\setminus\{4\}$.
\end{itemize}
\end{theorem}

In none of the cases addressed in Theorem~\ref{CnoRU} the
eigenvalues are roots of unity, so Equation~\eqref{E:MPerPerOfEndo}
implies $\MPer(f_A) = \Per(f_A)$.
\textit{These cases are listed in rows 12-15 of Table~2.}

\subsection{Real eigenvalues}

Real eigenvalues either come in pairs of irrational quadratic
integers (that is, zeros of polynomials of the shape $x^2 - tx +d$,
$t,d\in\ZZ$) or elements of $\ZZ$. The fact that rational
eigenvalues have to be integers is shown in the following lemma.

\begin{lemma}\label{L:rationalImpliesInt}
If $A$ has one (and thus two) rational eigenvalues, they are in fact
integers, hence the polynomial splits into two linear factors over
$\ZZ$.
\end{lemma}

\begin{proof}
Let $\frac{p_1}{q_1}$ and $\frac{p_2}{q_2}$ be the zeros of the
characteristic polynomial $\chi^{}_A(x)$. Without loss of
generality, we can assume that $\gcd(p_1,q_1) = \gcd(p_2,q_2)=1$. We
know that $\frac{p_1}{q_1} + \frac{p_2}{q_2} = \frac{p_1 q_2 + p_2
q_1}{q_1 q_2}= \tr(A) \in\ZZ$.

\smallskip

Consequently, the numerator $r$ has to be divisible by $q_1 q_2$,
hence it is divisible by both $q_1$ and $q_2$, or, equivalently, $r=
p_1 q_2 + p_2 q_1 \equiv 0 \mod q_i$, $i\in\{1,2\}$. But $r \equiv 0
\equiv p_1 q_2 \mod q_1$, whence $p_1 q_2$ is divisible by $q_1$. As
$\gcd(p_1,q_1)=1$ by assumption, one has $q_1 | q_2$. Considering
the equation modulo $q_2$ analogously gives $q_2 | q_1$, hence
$q\coloneqq q_1 =\pm q_2$. Furthermore, $\frac{p_1}{q_1} \cdot
\frac{p_2}{q_2} = \det(A)\in\ZZ$, thus $\pm q^2 | p_1 p_2$ such that
the assumed coprimality implies $q\in\{-1,1\}$.
\end{proof}

The following theorem is the summary of Propositions~4.18, 4.19 and
4.23 from \cite{ABLSS}.

\renewcommand{\labelenumi}{\textnormal{(\alph{enumi})}}
\begin{theorem}[\cite{ABLSS}]\label{T:realEV}
Let $A$ be in $\Mat(2,\ZZ)$ with real eigenvalues.

\begin{enumerate}
\item Suppose $A$ has eigenvalues, neither of which is $\pm1$.
If $d+t\notin\{0,-2\}$, then $\MPer(f_A)=\NN$.\label{realNotOne}

\item If $d=t=0$ then $\MPer(f_A) = \{1\}$.\label{nullnull}

\item Suppose $t+d\in\{0,-2\}$ and  $(t,d)\not= (0,0)$.
Then $\MPer(f_A) =\NN\setminus\{2\}$.
\end{enumerate}

\end{theorem}

In the situation of $(a)$ and $(b)$,
no root of unity is eigenvalue of the matrix $A$ and hence
$\MPer(f_A) = \Per(f_A)$.
\textit{The rows in Table~2 corresponding to Theorem~\ref{T:realEV} are 9, 16
and 17}.

\smallskip

So according to Equation \eqref{E:MPerPerOfEndo} and in view of
Theorem~\ref{T:realEV}, the only cases of real eigenvalues in which
$\MPer(f_A) \not= \Per(f_A)$ correspond to $\pm 1$ being among the
eigenvalues. As Lemma~\ref{L:rationalImpliesInt} tells us, the other
eigenvalue then has to be an integer as well. These cases will be
dealt with in the following section.

\section{Filling the gaps: the remaining cases}\label{S:completion}

The cases where the general theory of minimal period sets does not
immediately give the period set of the corresponding toral
endomorphism is the case when the eigenvalues are $1$ or $-1$
and some second integer, which is in fact decisive for the determination
of the period set.
The simple example of $\id$ and $\left(\begin{matrix}1&1\\0&1
\end{matrix}\right)$ shows that the same eigenvalues can a
priori imply different period sets, the former being $\{1\}$, the
latter $\NN$, although both matrices share the (double) eigenvalue
$1$.

\smallskip

Let $E = \{-2,-1,0,1\}$ and $\ord_n a$ the order of $a$ modulo $n$, that
is, the least integer $k>0$ such that $a^k\equiv 1 \mod n$.
The order $\ord_n (a)$ is well-defined for all $n\in\NN$, $n>1$, such that
$\gcd(a,n)=1$.

\begin{lemma}\label{L:ordersets}
Let $a\in\ZZ\setminus\{0\}$. Then
\[
P_a \coloneqq \{\ord_n a \mid n\in\NN\setminus\{1\}, \gcd(a,n)=1\}
\]
equals one of the following sets:

\begin{enumerate}
\item $\{1\}$ if $a=1$,

\item $\{1,2\}$ if $a=-1$,

\item $\NN\setminus\{2\}$ if $a=-2$,

\item $\NN\setminus\{1\}$ if $a=2$,

\item $\NN$ if $a\in\ZZ\setminus(\exSet\cup\{2\})$.
\end{enumerate}

\end{lemma}

\begin{proof}
The statements for $a=\pm 1$ are clear, so we exclude these cases
from our further considerations. We first check that $2\notin
P_{-2}$: if $(-2)^2 \equiv 1 \mod n$, clearly, $n| [(-2)^2 -1] = 3$,
so the only possible choice for $n$ is $3$ (as $1$ is excluded). But
$-2 \equiv 1 \mod 3$, and thus $\ord_{3} (-2) = 1$, whence $1\in
P_{-2}$ and $2\notin P_{-2}$ follows.

\smallskip

Next, we note that $1\notin P_{2}$, for $2\equiv 1 \mod n$ would
imply $n|(2-1)=1$; however, $1\in P_a$ for all other $a$ because $a
\equiv 1 \mod (a-1)$ if $a>2$ and $a \equiv 1 \mod (-a+1)$ if $a <
-1$.

\smallskip

We first consider the case where $a$ is positive and assume $a>2$
or $k>1$, such that $a^k-1 > 1$. Clearly, $a^k \equiv 1 \mod
(a^k-1)$, so assume there is a $d|k$, $d\not= k$, with $a^d \equiv 1
\mod (a^k-1)$. But then $(a^k - 1) | (a^d -1)$, which is not
possible for $d<k$, hence $\ord_{a^k-1} (a) =k$ and $k\in P_a$.

\smallskip

Next, consider the case where $a$ is negative and $k$ even, $a\not=
-2$ or $k\not= 2$. One has $a^k \equiv 1 \mod (a^k-1)$, and $(a^k -
1)| (a^d - 1)$ for the divisor $d = \ord_{a^k-1}(a)$ of $k$. If $d$
is even, this gives the same contradiction as above; if $d$ is odd,
one has $(a^k-1) | (-a^d+1)$ and thus $\abs{a}^k - \abs{a}^d \leq
2$. But the only positive integers $d,k$ with $d<k$ satisfying this
inequality are $k=2$, $d=1$ in the case $\abs{a} = 2$. For $a < -2$
and $k$ odd, one readily checks that $a^k \equiv 1 \mod (-a^k+1)$
and similar reasoning as above shows that $k$ is indeed the order
modulo $(-a^k+1)$. Hence it follows that if $\abs{a} > 2$ or $k>2$
then $k\in P_a$, and in summary, the lemma follows.
\end{proof}

We stipulate that $P^{}_0 = \emptyset$. Then we can formulate the
following

\begin{prop}\label{P:intEV}
Let $A$ be in $\Mat(2,\ZZ)$ and assume $A$ has the eigenvalues $a, b
\in \ZZ$. Then $\Per(f_A) \supset \{1\}\cup P_{a}\cup P_{b}$.
\end{prop}

\begin{proof}
According to Theorem~\ref{T:mgcd}, two matrices in $\Mat(2,\ZZ)$
induce the same orbit structure on the rational lattices $L_n$ for
all $n$, if trace, determinant and mgcd coincide. The square of the
mgcd always divides the discriminant, see Equation
\eqref{E:mgcdDivDiscr}, hence the set of possible triplets
$(\tr,\det,\mgcd)$ can be itemised explicitly. Fixing the trace and
the determinant as $\tr(A) = a+b, \det(A) = a\cdot b$, the
discriminant is $\Delta = \tr(A)^2 - 4\det(A) = (b-a)^2$, whence the
mgcd has to divide $b-a$. Consequently, one has an upper diagonal
matrix in the following set corresponding to each possible value of
the mgcd
\begin{equation}\label{E:normalForms}
\left\{\left(\begin{matrix}a & r\\0 & b\end{matrix}\right) \mid r^2
| \Delta \right\}.
\end{equation}
In other words, given an integer matrix $A$, there is some upper
diagonal matrix in the above set that has exactly the same orbit
structure on each of the finite sets $L_n$, $n\in\NN$. Furthermore,
the matrices $\left(\begin{matrix}a & r\\ 0 & b\end{matrix}\right)$
and $\left(\begin{matrix}b & r\\ 0 & a\end{matrix}\right)$ have the
same orbit structure on each $L_n$. But an upper diagonal matrix
$\left(\begin{matrix}d_1 & r\\0 & d_2\end{matrix}\right)$ clearly
has points of all orders contained in $P_{d_1}$ and $P_{d_2}$, as,
for instance, for $k\in P_{d_1}$, the point $(\frac{1}{n},0)$ has
period $k=\ord_n(d_1)$ and by the previous sentence, the roles of
$d_1$ and $d_2$ are interchangeable. Thus, for eigenvalues $a,b$,
the set $\Per(f_A)$ comprises the union $P_a \cup P_b$. Since the
point $(0,0)$ has period $1$ for every integer matrix, the claim
follows.
\end{proof}

\begin{remark}
Note that the eigenvalue $0$ does not contribute any periods. If
both eigenvalues are $0$, the matrix is nilpotent, and the only
periodic point is $(0,0)$. If the second eigenvalue is non-zero, it
has to be an integer, and it determines the period set according to
Lemma~\ref{L:ordersets} and Proposition~\ref{P:intEV}.
If the second eigenvalue is $1$ or $-1$, one has
$A^2=A$ or $A^3=A$, respectively, which immediately gives the period sets.
\textit{The cases with $0$ among the eigenvalues are treated in rows
9--11 of Table~2 if not covered by row 16 or 17.}

\smallskip

The symbol `$\supset$' in Proposition~\ref{P:intEV} cannot be replaced by an
equality sign, because a non-zero upper-diagonal entry $r$ may give
rise to additional periods, as in the aforementioned example of
$\id$ versus $\left(\begin{matrix}1 & 1\\ 0 & 1\end{matrix}\right)$,
as well as for the matrices
$-\id$ and $\left(\begin{matrix}-1 & \phantom{-}1\\ \phantom{-}0 & -1\end{matrix}\right)$.
These cases are covered by Proposition~3.6 in \cite{TP}, where the powers of
suitably parametrised $2\times2$ matrices are considered.
Using our local approach modulo $n$, one could restrict the considerations to upper
diagonal matrices as in Equation~\eqref{E:normalForms}, which, together with the Nielsen numbers
whenever they do not vanish, yield the period sets as listed in Table~2.
We note that the cases of a double eigenvalue $1$ or $-1$, respectively, are the
only ones in which the knowledge of the eigenvalues is not enough to determine
the period set of the endomorphism.
\textit{The cases corresponding to the eigenvalues $\pm 1$ are listed in rows 1--5 in Table~2.}
\end{remark}

With help of Proposition~\ref{P:intEV}, we can write down the period
set for all remaining cases where $1$ or $-1$ is among the
eigenvalues of the matrix.

\begin{coro}\label{C:evpm1}
   Let $(t,d)$ denote the pair of trace and determinant of
   $A\in\Mat(2,\ZZ)$.
   \begin{itemize}
   \item[(a)] If the eigenvalues are $-1, -d$, hence $t+d=-1$, $d\notin\{-1,0,1\}$
   the period set $\Per(f_A)$ is $\NN$.

   \item[(b)] If the eigenvalues are $-2, 1$, hence $t-d=1$, then
   $\Per(f_A) = \NN\setminus\{2\}$.

   \item[(c)] If the eigenvalues are $1,d$, hence $t-d = 1$,
   $(t,d)\not=(-1,-2)$,
   then $\Per(f_A) = \NN$.
   \end{itemize}
\end{coro}
\begin{proof}
   Case (a) and (c) immediately follow from Proposition~\ref{P:intEV};
   for (b), we note that for each $x$ with $A^2 x = x \mod 1$, one finds
   $A^2 x - \one = -A x + x = -(A-\id) x = 0 \mod 1$ by the Cayley-Hamilton
   Theorem,  so $x$ is a fixed point
   and therefore, $A$ does not admit any points of least period $2$.
\end{proof}

We state again that the cases treated in Corollary~\ref{C:evpm1} are
the ones in which $\Per(f_A)$ and $\MPer(f_A)$ significantly differ;
the latter can be found on page~30 in \cite{ABLSS}.
\\
\textit{Corollary~\ref{C:evpm1} yields the entries of rows 18--20 in
Table~2.}

\section*{Acknowledgements}

The first author is partially supported by a MCYT/FEDER grant
MTM2008--03437, an AGAUR grant number 2014SGR--568, an ICREA
Academia, two grants FP7-PEOPLE-2012-IRSES 316338 and 318999, and
FEDER-UNAB10-4E-378. The second author
gratefully acknowledges the funding of the four months stay at the
Universitat Aut\`{o}noma de Barcelona
within the project Rozvoj v\v{e}deck\'ych kapacit Slezsk\'e univerzity
v Opav\v{e} (CZ.1.07/2.3.00/30.0007).

config: arxiv


TITLE: program for eigenvalue calculation
QUESTION [0 upvotes]: I have a n x n matrix. I would like to
(a) take successively higher powers of the matrix and then multiply by projection vectors until the resulting vectors differ by only a scalar factor.
(b) calculate the dominant eigenvalue of the matrix to compare to (a)
and (c) calculate, using the same tactic as in (a), the dominant right and left eigenvectors.
This is too much work to do by hand, so my question is: can anyone recommend a program/language or package that would be ideal for the above calculations?
Thanks.

REPLY [2 votes]: You should check out a Computer Algebra System (CAS) and pick one that you like the interface for. There are commercial to open sourced - freeware ones and here is a comparison (many of the responses refer to these, but this is a nice list.
For example, Mathematica ($) or Maxima or SAGE (both free).
See: http://en.wikipedia.org/wiki/Comparison_of_computer_algebra_systems
Enjoy - A


TITLE: Codimension 1 immersions and Stiefel-Whitney classes
QUESTION [7 upvotes]: From Milnor and Stasheff:
If the $n$-dimensional manifold $M$ can be immersed in $\mathbb{R}^{n+1}$ show that each Stiefel-Whitney class $w_i(M)$ is equal to the $i$-fold cup product $w_1(M)^i$.
From the Whitney duality theorem we immediately have that the dual Stiefel-Whitney classes $\bar{w_i}(M)$ are zero for $i>1$. But I don't see how to use this to show that each class is a cup product of the first Stiefel-Whitney class.
Looking at the second half of the question which is to show that $\mathbb{R}P^n$ can be immersed in $\mathbb{R}^{n+1}$ only if $n=2^r-1$ or $2^r-2$ is not hard - the dual total Stiefel-Whitney classes can only be 1 or $1+a$. In the first case we get that the total Stiefel-Whitney classes must also be 1, which is true when $n=2^r-1$, and in the second we find $w(M)=1+a+a^2+ \cdots + a^n$, which is true if $n=2^r-2$  (I think that all works).
Is there any way to salvage an argument for the first part of the question from this? Indeed for a codimension 1 immersion the dual total Stiefel-Whitney class can only be 1 or $1+\bar{w_1}(M)$. But I can't see how this implies that $w_i(M) = w_1(M)^i$.
Any hints/tips?
Edit I think I actually had it written above! I really only need to worry about the case where $\bar{w_1}(M) \ne 0$, else all the non-zero Stiefel-Whitney classes are zero. So I can construct the formal inverse of $1+\bar{w_1}(M)$ which is given by
$$
\begin{eqnarray*}
w_1 &=& \bar{w_1} \\
w_2 &=& \bar{w_1}^2+\bar{w_2} = w_1^2 \\
w_3 &=& \bar{w_1}^3+\bar{w_3}=w_1^3

\end{eqnarray*}
$$
and in general $w_i(M) = w_1(M)^i$

REPLY [10 votes]: From the immersion $i:M\to \mathbb R^n$ you get the exact sequence of bundles on $M$ (in which $N$ denotes the normal bundle of the immersion)
$$0\to T(M)\to i^\ast(T\mathbb R^n)\to N\to 0 $$
Since the middle bundle is trivial you have (using Whitney multiplicativity)
$$w(T(M)).w(N)=w(i^\ast(T\mathbb R^n)=1  $$
so that [writing as usual $w(M)$ for $w(T(M))$]
$$w(M)=w(N)^{-1}=(1+w_1(N))^{-1}=1+w_1(N)+w_1(N)^2+\ldots+w_1(N)^{i}+\ldots (*)$$
and so $w_i(M)=w_1(N)^i (**) \;$ , which is not yet quite the result.  However, if you consider the component of degree one in the graded equality $(\ast)$ , you'll get $w_1(M)=w_1(N)$ and so finally putting this into $(**)$ , you obtain $w_i(M)=w_1(M)^i$, the desired equality.


text:
:: Binary Operations Applied to Finite Sequences
::  by Czes{\l}aw Byli\'nski

environ

 vocabularies XBOOLE_0, SUBSET_1, FUNCT_1, PARTFUN1, RELAT_1, ZFMISC_1,
      FUNCOP_1, TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, ORDINAL4, ARYTM_3, CARD_1,
      BINOP_1, SETWISEO, FINSEQOP, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      NAT_1, RELAT_1, EQREL_1, FUNCT_1, FINSEQ_1, RELSET_1, PARTFUN1, FUNCT_2,
      BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO;
 constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCOP_1, SETWISEO, NAT_1, FINSEQ_2,
      RELSET_1, EQREL_1, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, NAT_1,
      FINSEQ_2, ORDINAL1, FINSEQ_1, CARD_1, RELSET_1;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions BINOP_1;
 equalities BINOP_1, FUNCOP_1, FINSEQ_2;
 expansions BINOP_1;
 theorems ZFMISC_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, BINOP_1, SETWISEO,
      FINSEQ_2, FUNCT_3, RELAT_1, XBOOLE_0, CARD_1, TARSKI;
 schemes NAT_1, FINSEQ_2;

begin

reserve x,y for set;
reserve C,C9,D,D9,E for non empty set;
reserve c for Element of C;
reserve c9 for Element of C9;
reserve d,d1,d2,d3,d4,e for Element of D;
reserve d9 for Element of D9;

:: Auxiliary theorems

theorem Th1:
  for f being Function holds <:{},f:> = {} & <:f,{}:> = {}
proof
  let f be Function;
  dom <:{},f:> = dom {} /\ dom f & dom <:f,{}:> = dom f /\ dom {} by
FUNCT_3:def 7;
  hence thesis;
end;

theorem
  for f being Function holds [:{},f:] = {} & [:f,{}:] = {}
proof
  let f be Function;
  dom [:{},f:] = [:dom {},dom f:] & dom [:f,{}:] = [:dom f,dom {}:] by
FUNCT_3:def 8;
  hence thesis by ZFMISC_1:90;
end;

theorem Th3:
  for F,f being Function holds F.:({},f) = {} & F.:(f,{}) = {}
proof
  let F,f be Function;
  F.:({},f) = F*{} by Th1;
  hence thesis by Th1;
end;

theorem
  for F being Function holds F[:]({},x) = {}
proof
  let F be Function;
  F[:]({},x) = F.:({}, dom {} --> x);
  hence thesis by Th3;
end;

theorem
  for F being Function holds F[;](x,{}) = {}
proof
  let F be Function;
  F[;](x,{}) = F.:(dom {} --> x, {});
  hence thesis by Th3;
end;

theorem Th6:
  for X being set, x1,x2 being set holds <:X-->x1,X-->x2:> = X -->[ x1,x2]
proof
  let X be set, x1,x2 be set;
  set f = X-->x1, g = X-->x2;
  set fg = <:f,g:>;
  now
    per cases;
    suppose
A1:   X = {};
      thus thesis by A1;
    end;
    suppose
A2:   X <> {};
      rng fg c= [:{x1},{x2}:];
      then
A3:   rng fg c= {[x1,x2]} by ZFMISC_1:29;
      set x = the Element of X;
A4:   dom f = X & dom g = X;
      then
A5:   dom fg = X by FUNCT_3:50;
      f.x = x1 & g.x = x2 by A2,FUNCOP_1:7;
      then fg.x = [x1,x2] by A2,A4,FUNCT_3:49;
      then [x1,x2] in rng fg by A2,A5,FUNCT_1:def 3;
      then {[x1,x2]} c= rng fg by ZFMISC_1:31;
      then rng fg = {[x1,x2]} by A3,XBOOLE_0:def 10;
      hence thesis by A5,FUNCOP_1:9;
    end;
  end;
  hence thesis;
end;

theorem Th7:
  for F being Function,X being set, x1,x2 being set st [x1,x2] in
  dom F holds F.:(X-->x1,X-->x2) = X --> F.(x1,x2)
proof
  let F be Function, X be set, x1,x2 be set such that
A1: [x1,x2] in dom F;
  set f = X-->x1, g = X-->x2;
  thus F.:(f,g) = F*(X-->[x1,x2]) by Th6
    .= X --> F.(x1,x2) by A1,FUNCOP_1:17;
end;

reserve i,j for natural Number;
reserve F for Function of [:D,D9:],E;
reserve p,q for FinSequence of D,
  p9,q9 for FinSequence of D9;

definition
  let D,D9,E,F,p,p9;
  redefine func F.:(p,p9) -> FinSequence of E;
  coherence by FINSEQ_2:70;
end;

definition
  let D,D9,E,F,p,d9;
  redefine func F[:](p,d9) -> FinSequence of E;
  coherence by FINSEQ_2:83;
end;

definition
  let D,D9,E,F,d,p9;
  redefine func F[;](d,p9) -> FinSequence of E;
  coherence by FINSEQ_2:77;
end;

reserve f,f9 for Function of C,D,
  h for Function of D,E;

definition
  let D,E be set, p be FinSequence of D, h be Function of D,E;
  redefine func h*p -> FinSequence of E;
  coherence by FINSEQ_2:32;
end;

theorem Th8:
  h*(p^<*d*>) = (h*p)^<*h.d*>
proof
  set q = h*(p^<*d*>);
  set r = (h*p)^<*h.d*>;
  set i = len p + 1;
A1: len q = len(p^<*d*>) by FINSEQ_2:33;
A2: len(h*p) = len p by FINSEQ_2:33;
  len(p^<*d*>) = i by FINSEQ_2:16;
  then
A3: dom q = Seg i by A1,FINSEQ_1:def 3;
A4: now
    let j be Nat;
A5: Seg len p = dom p by FINSEQ_1:def 3;
A6: Seg len(h*p) = dom(h*p) by FINSEQ_1:def 3;
    assume
A7: j in dom q;
    now
      per cases by A3,A7,A5,FINSEQ_2:7;
      suppose
A8:     j in dom p;
        hence h.((p^<*d*>).j) = h.(p.j) by FINSEQ_1:def 7
          .= (h*p).j by A2,A5,A6,A8,FUNCT_1:12
          .= r.j by A2,A5,A6,A8,FINSEQ_1:def 7;
      end;
      suppose
A9:     j = i;
        hence h.((p^<*d*>).j) = h.d by FINSEQ_1:42
          .= r.j by A2,A9,FINSEQ_1:42;
      end;
    end;
    hence q.j = r.j by A7,FUNCT_1:12;
  end;
  len r = len(h*p)+1 by FINSEQ_2:16;
  hence thesis by A1,A2,A4,FINSEQ_2:9,16;
end;

theorem
  h*(p^q) = (h*p)^(h*q)
proof
  defpred P[FinSequence of D] means h*(p^$1) = (h*p)^(h*$1);
A1: for q,d st P[q] holds P[q^<*d*>]
  proof
    let q,d such that
A2: h*(p^q) = (h*p)^(h*q);
    thus h*(p^(q^<*d*>)) = h*((p^q)^<*d*>) by FINSEQ_1:32
      .= (h*(p^q))^<*h.d*> by Th8
      .= (h*p)^((h*q)^<*h.d*>) by A2,FINSEQ_1:32
      .= (h*p)^(h*(q^<*d*>)) by Th8;
  end;
  h*(p^<*>D) = h*p by FINSEQ_1:34
    .= (h*p)^(h*(<*>D)) by FINSEQ_1:34;
  then
A3: P[<*>D];
  for q holds P[q] from FINSEQ_2:sch 2(A3,A1);
  hence thesis;
end;

reserve T,T1,T2,T3 for Tuple of i,D;
reserve T9 for Tuple of i, D9;
reserve S for Tuple of j, D;
reserve S9 for Tuple of j, D9;

Lm1: for T being Tuple of 0, D holds F.:(T,T9) = <*>E
proof
  let T be Tuple of 0, D;
  T = <*>D;
  hence thesis by FINSEQ_2:73;
end;

Lm2: for T9 being Tuple of 0, D9 holds F[;](d,T9) = <*>E
proof
  let T9 be Tuple of 0, D9;
  T9 = <*>D9;
  hence thesis by FINSEQ_2:79;
end;

Lm3: for T being Tuple of 0, D holds F[:](T,d9) = <*>E
proof
  let T be Tuple of 0, D;
  T = <*>D;
  hence thesis by FINSEQ_2:85;
end;

theorem Th10:
  F.:(T^<*d*>,T9^<*d9*>) = (F.:(T,T9))^<*F.(d,d9)*>
proof
  set p = T^<*d*>, q = T9^<*d9*>, pq = F.:(T,T9);
  set r = F.:(p,q), s = pq^<*F.(d,d9)*>;
A1: len T9 = i by CARD_1:def 7;
  then
A2: len q = i+1 by FINSEQ_2:16;
A3: len T = i by CARD_1:def 7;
  then
A4: len pq = i by A1,FINSEQ_2:72;
  len p = i+1 by A3,FINSEQ_2:16;
  then
A5: len r = i+1 by A2,FINSEQ_2:72;
  then
A6: dom r = Seg(i+1) by FINSEQ_1:def 3;
A7: now
    let j be Nat;
    assume
A8: j in dom r;
    now
      per cases by A6,A8,FINSEQ_2:7;
      suppose
A9:     j in Seg i;
        Seg len T = dom T by FINSEQ_1:def 3;
        then
A10:    p.j = T.j by A3,A9,FINSEQ_1:def 7;
A11:    Seg len pq = dom pq by FINSEQ_1:def 3;
        Seg len T9 = dom T9 by FINSEQ_1:def 3;
        then
A12:    q.j = T9.j by A1,A9,FINSEQ_1:def 7;
        j in dom pq by A4,A9,FINSEQ_1:def 3;
        hence F.(p.j,q.j) = pq.j by A10,A12,FUNCOP_1:22
          .= s.j by A4,A9,A11,FINSEQ_1:def 7;
      end;
      suppose
A13:    j = i+1;
        then p.j = d & q.j = d9 by A3,A1,FINSEQ_1:42;
        hence F.(p.j,q.j) = s.j by A4,A13,FINSEQ_1:42;
      end;
    end;
    hence r.j = s.j by A8,FUNCOP_1:22;
  end;
  len s = len pq + 1 by FINSEQ_2:16;
  hence thesis by A5,A4,A7,FINSEQ_2:9;
end;

theorem
  F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9))
proof
A0: i is Nat & j is Nat by TARSKI:1;
  defpred P[Nat] means for S being Tuple of $1, D, S9 being Tuple
  of $1, D9 holds F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9));
  now
    let j such that
A1: for S,S9 holds F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9));
    let S be Tuple of j+1, D;
    let S9 be Tuple of j+1, D9;
    consider S1 being Element of j-tuples_on D, d such that
A2: S = S1^<*d*> by FINSEQ_2:117;
A3: T^S = T^S1^<*d*> by A2,FINSEQ_1:32;
    reconsider S1 as Tuple of j, D;
    consider S19 being Element of j-tuples_on D9, d9 such that
A4: S9 = S19^<*d9*> by FINSEQ_2:117;
A5: T9^S9 = T9^S19^<*d9*> by A4,FINSEQ_1:32;
    reconsider S19 as Tuple of j, D9;
    thus F.:(T^S,T9^S9) = (F.:(T^S1,T9^S19))^<*F.(d,d9)*> by A3,A5,Th10
      .= (F.:(T,T9))^(F.:(S1,S19))^<*F.(d,d9)*> by A1
      .= (F.:(T,T9))^((F.:(S1,S19))^<*F.(d,d9)*>) by FINSEQ_1:32
      .= (F.:(T,T9))^(F.:(S,S9)) by A2,A4,Th10;
  end;
  then
A6: for j be Nat st P[j] holds P[j+1];
  now
    let S be Tuple of 0, D;
    let S9 be Tuple of 0, D9;
    S = <*>D;
    then
A7: F.:(S,S9) = <*>E by FINSEQ_2:73;
    T^S = T & T9^S9 = T9 by FINSEQ_2:95;
    hence F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9)) by A7,FINSEQ_1:34;
  end;
  then
A8: P[0];
  for j be Nat holds P[j] from NAT_1:sch 2(A8,A6);
  hence thesis by A0;
end;

theorem Th12:
  F[;](d,p9^<*d9*>) = (F[;](d,p9))^<*F.(d,d9)*>
proof
  set pd = p9^<*d9*>, q = F[;](d,p9);
  set r = F[;](d,pd), s = q^<*F.(d,d9)*>;
  set i = len p9;
A1: len q = i by FINSEQ_2:78;
  len pd = i + 1 by FINSEQ_2:16;
  then
A2: len r = i + 1 by FINSEQ_2:78;
  then
A3: dom r = Seg(i+1) by FINSEQ_1:def 3;
A4: now
    let j be Nat;
    assume
A5: j in dom r;
    now
      per cases by A3,A5,FINSEQ_2:7;
      suppose
A6:     j in Seg i;
        then
A7:     j in dom q by A1,FINSEQ_1:def 3;
A8:     Seg len q = dom q by FINSEQ_1:def 3;
        Seg len p9 = dom p9 by FINSEQ_1:def 3;
        hence F.(d,pd.j) = F.(d,p9.j) by A6,FINSEQ_1:def 7
          .= q.j by A7,FUNCOP_1:32
          .= s.j by A1,A6,A8,FINSEQ_1:def 7;
      end;
      suppose
A9:     j = i+1;
        hence F.(d,pd.j) = F.(d,d9) by FINSEQ_1:42
          .= s.j by A1,A9,FINSEQ_1:42;
      end;
    end;
    hence r.j = s.j by A5,FUNCOP_1:32;
  end;
  len s = len q + 1 by FINSEQ_2:16;
  hence thesis by A1,A2,A4,FINSEQ_2:9;
end;

theorem
  F[;](d,p9^q9) = (F[;](d,p9))^(F[;](d,q9))
proof
  defpred P[FinSequence of D9] means F[;](d,p9^($1)) = (F[;](d,p9))^(F[;](d,$1
  ));
A1: for q9,d9 st P[q9] holds P[q9^<*d9*>]
  proof
    let q9,d9 such that
A2: F[;](d,p9^q9) = (F[;](d,p9))^(F[;](d,q9));
    thus F[;](d,p9^(q9^<*d9*>)) = F[;](d,(p9^q9)^<*d9*>) by FINSEQ_1:32
      .= (F[;](d,p9^q9))^<*F.(d,d9)*> by Th12
      .= (F[;](d,p9))^((F[;](d,q9))^<*F.(d,d9)*>) by A2,FINSEQ_1:32
      .= (F[;](d,p9))^(F[;](d,q9^<*d9*>)) by Th12;
  end;
  F[;](d,p9^(<*>D9)) = F[;](d,p9) by FINSEQ_1:34
    .= (F[;](d,p9))^(<*>E) by FINSEQ_1:34
    .= (F[;](d,p9))^(F[;](d,<*>D9)) by FINSEQ_2:79;
  then
A3: P[<*>D9];
  for q9 holds P[q9] from FINSEQ_2:sch 2(A3,A1);
  hence thesis;
end;

theorem Th14:
  F[:](p^<*d*>,d9) = (F[:](p,d9))^<*F.(d,d9)*>
proof
  set pd = p^<*d*>, q = F[:](p,d9);
  set r = F[:](pd,d9), s = q^<*F.(d,d9)*>;
  set i = len p;
A1: len q = i by FINSEQ_2:84;
  len pd = i + 1 by FINSEQ_2:16;
  then
A2: len r = i + 1 by FINSEQ_2:84;
  then
A3: dom r = Seg(i+1) by FINSEQ_1:def 3;
A4: now
    let j be Nat;
    assume
A5: j in dom r;
    now
      per cases by A3,A5,FINSEQ_2:7;
      suppose
A6:     j in Seg i;
        then
A7:     j in dom q by A1,FINSEQ_1:def 3;
        Seg len p = dom p by FINSEQ_1:def 3;
        hence F.(pd.j,d9) = F.(p.j,d9) by A6,FINSEQ_1:def 7
          .= q.j by A7,FUNCOP_1:27
          .= s.j by A7,FINSEQ_1:def 7;
      end;
      suppose
A8:     j = i+1;
        hence F.(pd.j,d9) = F.(d,d9) by FINSEQ_1:42
          .= s.j by A1,A8,FINSEQ_1:42;
      end;
    end;
    hence r.j = s.j by A5,FUNCOP_1:27;
  end;
  len s = len q + 1 by FINSEQ_2:16;
  hence thesis by A1,A2,A4,FINSEQ_2:9;
end;

theorem
  F[:](p^q,d9) = (F[:](p,d9))^(F[:](q,d9))
proof
  defpred P[FinSequence of D] means F[:](p^($1),d9) = (F[:](p,d9))^(F[:]($1,d9
  ));
A1: for q,d st P[q] holds P[q^<*d*>]
  proof
    let q,d such that
A2: F[:](p^q,d9) = (F[:](p,d9))^(F[:](q,d9));
    thus F[:](p^(q^<*d*>),d9) = F[:]((p^q)^<*d*>,d9) by FINSEQ_1:32
      .= (F[:](p^q,d9))^<*F.(d,d9)*> by Th14
      .= (F[:](p,d9))^((F[:](q,d9))^<*F.(d,d9)*>) by A2,FINSEQ_1:32
      .= (F[:](p,d9))^(F[:](q^<*d*>,d9)) by Th14;
  end;
  F[:](p^(<*>D),d9) = F[:](p,d9) by FINSEQ_1:34
    .= (F[:](p,d9))^(<*>E) by FINSEQ_1:34
    .= (F[:](p,d9))^(F[:](<*>D,d9)) by FINSEQ_2:85;
  then
A3: P[<*>D];
  for q holds P[q] from FINSEQ_2:sch 2(A3,A1);
  hence thesis;
end;

theorem
  for h being Function of D,E holds h*(i|->d) = i|->(h.d)
proof
  let h be Function of D,E;
  d in D;
  then d in dom h by FUNCT_2:def 1;
  hence thesis by FUNCOP_1:17;
end;

theorem Th17:
  F.:(i|->d,i|->d9) = i |-> (F.(d,d9))
proof
  [d,d9] in [:D,D9:] by ZFMISC_1:def 2;
  then [d,d9] in dom F by FUNCT_2:def 1;
  hence thesis by Th7;
end;

theorem
  F[;](d,i|->d9) = i |-> (F.(d,d9))
proof
  thus F[;](d,i|->d9) = F.:(i |->d,i|->d9)
    .= i |-> (F.(d,d9)) by Th17;
end;

theorem
  F[:](i|->d,d9) = i |-> (F.(d,d9))
proof
  thus F[:](i|->d,d9) = F.:(i |->d,i|->d9)
    .= i |-> (F.(d,d9)) by Th17;
end;

theorem
  F.:(i|->d,T9) = F[;](d,T9)
proof
  dom T9 = Seg len T9 by FINSEQ_1:def 3
    .= Seg i by CARD_1:def 7;
  hence thesis;
end;

theorem
  F.:(T,i|->d) = F[:](T,d)
proof
  dom T = Seg len T by FINSEQ_1:def 3
    .= Seg i by CARD_1:def 7;
  hence thesis;
end;

theorem
  F[;](d,T9) = F[;](d,id D9)*T9
proof
  rng T9 c= D9;
  hence F[;](d,T9) = F[;](d,(id D9)*T9) by RELAT_1:53
    .= F[;](d,(id D9))*T9 by FUNCOP_1:34;
end;

theorem
  F[:](T,d) = F[:](id D,d)*T
proof
  rng T c= D;
  hence F[:](T,d) = F[:]((id D)*T,d) by RELAT_1:53
    .= F[:]((id D),d)*T by FUNCOP_1:29;
end;

:: Binary Operations

reserve F,G for BinOp of D;
reserve u for UnOp of D;
reserve H for BinOp of E;

Lm4: T is Function of Seg i,D
proof
  len T = i by CARD_1:def 7;
  then Seg i = dom T by FINSEQ_1:def 3;
  hence thesis by FINSEQ_2:26;
end;

theorem Th24:
  F is associative implies F[;](d,id D)*(F.:(f,f9)) = F.:(F[;](d, id D)*f,f9)
proof
  assume
A1: F is associative;
  now
    let c;
    thus (F[;](d,id D)*(F.:(f,f9))).c = (F[;](d,id D)).((F.:(f,f9)).c) by
FUNCT_2:15
      .= (F[;](d,id D)).(F.(f.c,f9.c)) by FUNCOP_1:37
      .= F.(d,(id D).(F.(f.c,f9.c))) by FUNCOP_1:53
      .= F.(d,F.(f.c,f9.c))
      .= F.(F.(d,f.c),f9.c) by A1
      .= F.((F[;](d,f)).c,f9.c) by FUNCOP_1:53
      .= F.(((F[;](d,id D))*f).c,f9.c) by FUNCOP_1:55
      .= (F.:(F[;](d,id D)*f,f9)).c by FUNCOP_1:37;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th25:
  F is associative implies F[:](id D,d)*(F.:(f,f9)) = F.:(f,F[:]( id D,d)*f9)
proof
  assume
A1: F is associative;
  now
    let c;
    thus (F[:](id D,d)*(F.:(f,f9))).c = (F[:](id D,d)).((F.:(f,f9)).c) by
FUNCT_2:15
      .= (F[:](id D,d)).(F.(f.c,f9.c)) by FUNCOP_1:37
      .= F.((id D).(F.(f.c,f9.c)),d) by FUNCOP_1:48
      .= F.(F.(f.c,f9.c),d)
      .= F.(f.c,F.(f9.c,d)) by A1
      .= F.(f.c,(F[:](f9,d)).c) by FUNCOP_1:48
      .= F.(f.c,((F[:](id D,d))*f9).c) by FUNCOP_1:50
      .= (F.:(f,F[:](id D,d)*f9)).c by FUNCOP_1:37;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  F is associative implies F[;](d,id D)*(F.:(T1,T2)) = F.:(F[;](d,id D)*
  T1,T2 )
proof
  assume
A1: F is associative;
  per cases;
  suppose
A2: i = 0;
    then F.:(T1,T2) = <*>D by Lm1;
    then
A3: F[;](d,id D)*(F.:(T1,T2)) = <*>D;
    T2 = <*>D by A2;
    hence thesis by A3,FINSEQ_2:73;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T1 is Function of C,D & T2 is Function of C,D by Lm4;
    hence thesis by A1,Th24;
  end;
end;

theorem
  F is associative implies F[:](id D,d)*(F.:(T1,T2)) = F.:(T1,F[:](id D,
  d)*T2 )
proof
  assume
A1: F is associative;
  per cases;
  suppose
A2: i = 0;
    then F.:(T1,T2) = <*>D by Lm1;
    then
A3: F[:](id D,d)*(F.:(T1,T2)) = <*>D;
    T1 = <*>D by A2;
    hence thesis by A3,FINSEQ_2:73;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T1 is Function of C,D & T2 is Function of C,D by Lm4;
    hence thesis by A1,Th25;
  end;
end;

theorem
  F is associative implies F.:(F.:(T1,T2),T3) = F.:(T1,F.:(T2,T3))
proof
  assume
A1: F is associative;
  per cases;
  suppose
A2: i = 0;
    then F.:(T1,T2) = <*>D by Lm1;
    then
A3: F.:(F.:(T1,T2),T3) = <*>D by FINSEQ_2:73;
    F.:(T2,T3) = <*>D by A2,Lm1;
    hence thesis by A3,FINSEQ_2:73;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
A4: T3 is Function of C,D by Lm4;
    T1 is Function of C,D & T2 is Function of C,D by Lm4;
    hence thesis by A1,A4,FUNCOP_1:61;
  end;
end;

theorem
  F is associative implies F[:](F[;](d1,T),d2) = F[;](d1,F[:](T,d2))
proof
  assume
A1: F is associative;
  per cases;
  suppose
A2: i = 0;
    then F[;](d1,T) = <*>D by Lm2;
    then
A3: F[:](F[;](d1,T),d2) = <*>D by FINSEQ_2:85;
    F[:](T,d2) = <*>D by A2,Lm3;
    hence thesis by A3,FINSEQ_2:79;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,FUNCOP_1:59;
  end;
end;

theorem
  F is associative implies F.:(F[:](T1,d),T2) = F.:(T1,F[;](d,T2))
proof
  assume
A1: F is associative;
  per cases;
  suppose
A2: i = 0;
    then F[:](T1,d) = <*>D by Lm3;
    then
A3: F.:(F[:](T1,d),T2) = <*>D by FINSEQ_2:73;
    F[;](d,T2) = <*>D by A2,Lm2;
    hence thesis by A3,FINSEQ_2:73;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T1 is Function of C,D & T2 is Function of C,D by Lm4;
    hence thesis by A1,FUNCOP_1:60;
  end;
end;

theorem
  F is associative implies F[;](F.(d1,d2),T) = F[;](d1,F[;](d2,T))
proof
  assume
A1: F is associative;
  per cases;
  suppose
    i = 0;
    then T = <*>D & F[;](d2,T) = <*>D by Lm2;
    hence thesis;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,FUNCOP_1:62;
  end;
end;

theorem
  F is associative implies F[:](T,F.(d1,d2)) = F[:](F[:](T,d1),d2)
proof
  assume
A1: F is associative;
  per cases;
  suppose
    i = 0;
    then T = <*>D & F[:](T,d1) = <*>D by Lm3;
    hence thesis;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,FUNCOP_1:63;
  end;
end;

theorem
  F is commutative implies F.:(T1,T2) = F.:(T2,T1)
proof
  assume
A1: F is commutative;
  per cases;
  suppose
A2: i = 0;
    then F.:(T1,T2) = <*>D by Lm1;
    hence thesis by A2,Lm1;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T1 is Function of C,D & T2 is Function of C,D by Lm4;
    hence thesis by A1,FUNCOP_1:65;
  end;
end;

theorem
  F is commutative implies F[;](d,T) = F[:](T,d)
proof
  assume
A1: F is commutative;
  per cases;
  suppose
A2: i = 0;
    then F[;](d,T) = <*>D by Lm2;
    hence thesis by A2,Lm3;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,FUNCOP_1:64;
  end;
end;

theorem Th35:
  F is_distributive_wrt G implies F[;](G.(d1,d2),f) = G.:(F[;](d1,
  f),F[;] (d2,f))
proof
  assume
A1: F is_distributive_wrt G;
  now
    let c;
    thus (F[;](G.(d1,d2),f)).c = F.(G.(d1,d2),f.c) by FUNCOP_1:53
      .= G.(F.(d1,f.c),F.(d2,f.c)) by A1,BINOP_1:11
      .= G.(F[;](d1,f).c,F.(d2,f.c)) by FUNCOP_1:53
      .= G.((F[;](d1,f)).c,(F[;](d2,f)).c) by FUNCOP_1:53
      .= (G.:(F[;](d1,f),F[;](d2,f))).c by FUNCOP_1:37;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th36:
  F is_distributive_wrt G implies F[:](f,G.(d1,d2)) = G.:(F[:](f,
  d1),F[:] (f,d2))
proof
  assume
A1: F is_distributive_wrt G;
  now
    let c;
    thus (F[:](f,G.(d1,d2))).c = F.(f.c,G.(d1,d2)) by FUNCOP_1:48
      .= G.(F.(f.c,d1),F.(f.c,d2)) by A1,BINOP_1:11
      .= G.(F[:](f,d1).c,F.(f.c,d2)) by FUNCOP_1:48
      .= G.((F[:](f,d1)).c,(F[:](f,d2)).c) by FUNCOP_1:48
      .= (G.:(F[:](f,d1),F[:](f,d2))).c by FUNCOP_1:37;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th37:
  (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F.:(f
  ,f9)) = H.:(h*f,h*f9)
proof
  assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
  now
    let c;
    thus (h*(F.:(f,f9))).c = h.((F.:(f,f9)).c) by FUNCT_2:15
      .= h.(F.(f.c,f9.c)) by FUNCOP_1:37
      .= H.(h.(f.c),h.(f9.c)) by A1
      .= H.((h*f).c,h.(f9.c)) by FUNCT_2:15
      .= H.((h*f).c,(h*f9).c) by FUNCT_2:15
      .= (H.:(h*f,h*f9)).c by FUNCOP_1:37;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th38:
  (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[;](
  d,f)) = H[;](h.d,h*f)
proof
  assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
  reconsider g = C --> d as Function of C,D;
A2: dom h = D & dom(h*f) = C by FUNCT_2:def 1;
  thus h*(F[;](d,f)) = h*(F.:(g,f)) by FUNCT_2:def 1
    .= H.:(h*g,h*f) by A1,Th37
    .= H[;](h.d,h*f) by A2,FUNCOP_1:17;
end;

theorem Th39:
  (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[:](
  f,d)) = H[:](h*f,h.d)
proof
  assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
  reconsider g = C --> d as Function of C,D;
A2: dom h = D & dom(h*f) = C by FUNCT_2:def 1;
  thus h*(F[:](f,d)) = h*(F.:(f,g)) by FUNCT_2:def 1
    .= H.:(h*f,h*g) by A1,Th37
    .= H[:](h*f,h.d) by A2,FUNCOP_1:17;
end;

theorem
  u is_distributive_wrt F implies u*(F.:(f,f9)) = F.:(u*f,u*f9)
by Th37;

theorem
  u is_distributive_wrt F implies u*(F[;](d,f)) = F[;](u.d,u*f)
by Th38;

theorem
  u is_distributive_wrt F implies u*(F[:](f,d)) = F[:](u*f,u.d)
by Th39;

theorem Th43:
  F is having_a_unity implies F.:(C-->the_unity_wrt F,f) = f & F.:
  (f,C-->the_unity_wrt F) = f
proof
  set e = the_unity_wrt F;
  reconsider g = C-->e as Function of C,D;
  assume
A1: F is having_a_unity;
  now
    let c;
    thus (F.:(g,f)).c = F.(g.c,f.c) by FUNCOP_1:37
      .= F.(e,f.c)
      .= f.c by A1,SETWISEO:15;
  end;
  hence F.:(C-->e,f) = f by FUNCT_2:63;
  now
    let c;
    thus (F.:(f,g)).c = F.(f.c,g.c) by FUNCOP_1:37
      .= F.(f.c,e)
      .= f.c by A1,SETWISEO:15;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th44:
  F is having_a_unity implies F[;](the_unity_wrt F,f) = f
proof
  set e = the_unity_wrt F;
  assume
A1: F is having_a_unity;
  now
    let c;
    thus (F[;](e,f)).c = F.(e,f.c) by FUNCOP_1:53
      .= f.c by A1,SETWISEO:15;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th45:
  F is having_a_unity implies F[:](f,the_unity_wrt F) = f
proof
  set e = the_unity_wrt F;
  assume
A1: F is having_a_unity;
  now
    let c;
    thus (F[:](f,e)).c = F.(f.c,e) by FUNCOP_1:48
      .= f.c by A1,SETWISEO:15;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  F is_distributive_wrt G implies F[;](G.(d1,d2),T) = G.:(F[;](d1,T),F
  [;] (d2,T))
proof
  assume
A1: F is_distributive_wrt G;
  per cases;
  suppose
    i = 0;
    then F[;](d1,T) = <*>D & F[;](G.(d1,d2),T) = <*>D by Lm2;
    hence thesis by FINSEQ_2:73;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th35;
  end;
end;

theorem
  F is_distributive_wrt G implies F[:](T,G.(d1,d2)) = G.:(F[:](T,d1),F
  [:] (T,d2))
proof
  assume
A1: F is_distributive_wrt G;
  per cases;
  suppose
    i = 0;
    then F[:](T,d1) = <*>D & F[:](T,G.(d1,d2)) = <*>D by Lm3;
    hence thesis by FINSEQ_2:73;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th36;
  end;
end;

theorem Th48:
  (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F.:(
  T1,T2)) = H.:(h*T1,h*T2)
proof
  assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
  per cases;
  suppose
A2: i = 0;
    then F.:(T1,T2) = <*>D by Lm1;
    then
A3: h*(F.:(T1,T2)) = <*>E;
    h*T1 = <*>E by A2;
    hence thesis by A3,FINSEQ_2:73;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T1 is Function of C,D & T2 is Function of C,D by Lm4;
    hence thesis by A1,Th37;
  end;
end;

theorem Th49:
  (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[;](
  d,T)) = H[;](h.d,h*T)
proof
  assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
  per cases;
  suppose
A2: i = 0;
    then F[;](d,T) = <*>D by Lm2;
    then
A3: h*(F[;](d,T)) = <*>E;
    h*T = <*>E by A2;
    hence thesis by A3,FINSEQ_2:79;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th38;
  end;
end;

theorem Th50:
  (for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[:](
  T,d)) = H[:](h*T,h.d)
proof
  assume
A1: for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2);
  per cases;
  suppose
A2: i = 0;
    then F[:](T,d) = <*>D by Lm3;
    then
A3: h*(F[:](T,d)) = <*>E;
    h*T = <*>E by A2;
    hence thesis by A3,FINSEQ_2:85;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th39;
  end;
end;

theorem
  u is_distributive_wrt F implies u*(F.:(T1,T2)) = F.:(u*T1,u*T2)
by Th48;

theorem
  u is_distributive_wrt F implies u*(F[;](d,T)) = F[;](u.d,u*T)
by Th49;

theorem
  u is_distributive_wrt F implies u*(F[:](T,d)) = F[:](u*T,u.d)
by Th50;

theorem
  G is_distributive_wrt F & u = G[;](d,id D) implies u is_distributive_wrt F
proof
  assume that
A1: G is_distributive_wrt F and
A2: u = G[;](d,id D);
  let d1,d2;
  thus u.(F.(d1,d2)) = G.(d,(id D).(F.(d1,d2))) by A2,FUNCOP_1:53
    .= G.(d,F.(d1,d2))
    .= F.(G.(d,d1),G.(d,d2)) by A1,BINOP_1:11
    .= F.(G.(d,(id D).d1),G.(d,d2))
    .= F.(G.(d,(id D).d1),G.(d,(id D).d2))
    .= F.(u.d1,G.(d,(id D).d2)) by A2,FUNCOP_1:53
    .= F.(u.d1,u.d2) by A2,FUNCOP_1:53;
end;

theorem
  G is_distributive_wrt F & u = G[:](id D,d) implies u is_distributive_wrt F
proof
  assume that
A1: G is_distributive_wrt F and
A2: u = G[:](id D,d);
  let d1,d2;
  thus u.(F.(d1,d2)) = G.((id D).(F.(d1,d2)),d) by A2,FUNCOP_1:48
    .= G.(F.(d1,d2),d)
    .= F.(G.(d1,d),G.(d2,d)) by A1,BINOP_1:11
    .= F.(G.((id D).d1,d),G.(d2,d))
    .= F.(G.((id D).d1,d),G.((id D).d2,d))
    .= F.(u.d1,G.((id D).d2,d)) by A2,FUNCOP_1:48
    .= F.(u.d1,u.d2) by A2,FUNCOP_1:48;
end;

theorem
  F is having_a_unity implies
  F.:(i|->the_unity_wrt F,T) = T & F.:(T,i|->the_unity_wrt F) = T
proof
  assume
A1: F is having_a_unity;
  per cases;
  suppose
A2: i = 0;
    then T = <*>D;
    hence thesis by A2,Lm1;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th43;
  end;
end;

theorem
  F is having_a_unity implies F[;](the_unity_wrt F,T) = T
proof
  assume
A1: F is having_a_unity;
  per cases;
  suppose
 i = 0;
    then T = <*>D;
    hence thesis by Lm2;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th44;
  end;
end;

theorem
  F is having_a_unity implies F[:](T,the_unity_wrt F) = T
proof
  assume
A1: F is having_a_unity;
  per cases;
  suppose
 i = 0;
    then T = <*>D;
    hence thesis by Lm3;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th45;
  end;
end;

definition
  let D,u,F;
  pred u is_an_inverseOp_wrt F means

  for d holds F.(d,u.d) = the_unity_wrt F & F.(u.d,d) = the_unity_wrt F;
end;

definition
  let D,F;
  attr F is having_an_inverseOp means

  ex u st u is_an_inverseOp_wrt F;
end;

definition
  let D,F;
  assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp;
  func the_inverseOp_wrt F -> UnOp of D means
  :Def3:
  it is_an_inverseOp_wrt F;
  existence by A3;
  uniqueness
  proof
    set e = the_unity_wrt F;
    let u1,u2 be UnOp of D such that
A4: for d holds F.(d,u1.d) = e & F.(u1.d,d) = e and
A5: for d holds F.(d,u2.d) = e & F.(u2.d,d) = e;
    now
      let d;
      set d1 = u1.d, d2 = u2.d;
      thus u1.d = F.(d1,e) by A1,SETWISEO:15
        .= F.(d1,F.(d,d2)) by A5
        .= F.(F.(d1,d),d2) by A2
        .= F.(e,d2) by A4
        .= u2.d by A1,SETWISEO:15;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

theorem Th59:
  F is having_a_unity & F is associative & F is
having_an_inverseOp implies F.((the_inverseOp_wrt F).d,d) = the_unity_wrt F & F
  .(d,(the_inverseOp_wrt F).d) = the_unity_wrt F
proof
  assume F is having_a_unity & F is associative & F is having_an_inverseOp;
  then the_inverseOp_wrt F is_an_inverseOp_wrt F by Def3;
  hence thesis;
end;

theorem Th60:
  F is having_a_unity & F is associative & F is
  having_an_inverseOp & F.(d1,d2) = the_unity_wrt F implies d1 = (
  the_inverseOp_wrt F).d2 & (the_inverseOp_wrt F).d1 = d2
proof
  assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: F.(d1,d2) = the_unity_wrt F;
  set e = the_unity_wrt F, d3 = (the_inverseOp_wrt F).d2;
  F.(F.(d1,d2),d3) = d3 by A1,A4,SETWISEO:15;
  then F.(d1,F.(d2,d3)) = d3 by A2;
  then F.(d1,e) = d3 by A1,A2,A3,Th59;
  hence d1 = d3 by A1,SETWISEO:15;
  set d3 = (the_inverseOp_wrt F).d1;
  F.(d3,F.(d1,d2)) = d3 by A1,A4,SETWISEO:15;
  then F.(F.(d3,d1),d2) = d3 by A2;
  then F.(e,d2) = d3 by A1,A2,A3,Th59;
  hence thesis by A1,SETWISEO:15;
end;

theorem Th61:
  F is having_a_unity & F is associative & F is
  having_an_inverseOp implies (the_inverseOp_wrt F).(the_unity_wrt F) =
  the_unity_wrt F
proof
  assume that
A1: F is having_a_unity and
A2: F is associative & F is having_an_inverseOp;
  set e = the_unity_wrt F;
  F.(e,e) = e by A1,SETWISEO:15;
  hence thesis by A1,A2,Th60;
end;

theorem Th62:
  F is having_a_unity & F is associative & F is
having_an_inverseOp implies (the_inverseOp_wrt F).((the_inverseOp_wrt F).d) = d
proof
  assume
A1: F is having_a_unity & F is associative & F is having_an_inverseOp;
  then F.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F by Th59;
  hence thesis by A1,Th60;
end;

theorem Th63:
  F is having_a_unity & F is associative & F is commutative & F is
  having_an_inverseOp implies (the_inverseOp_wrt F) is_distributive_wrt F
proof
  assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is commutative and
A4: F is having_an_inverseOp;
  let d1,d2;
  set e = the_unity_wrt F, u = the_inverseOp_wrt F;
  F.(F.(u.d1,u.d2),F.(d1,d2)) = F.(u.d1,F.(u.d2,F.(d1,d2))) by A2
    .= F.(u.d1,F.(F.(u.d2,d1),d2)) by A2
    .= F.(u.d1,F.(F.(d1,u.d2),d2)) by A3
    .= F.(u.d1,F.(d1,F.(u.d2,d2))) by A2
    .= F.(u.d1,F.(d1,e)) by A1,A2,A4,Th59
    .= F.(F.(u.d1,d1),e) by A2
    .= F.(e,e) by A1,A2,A4,Th59
    .= e by A1,SETWISEO:15;
  hence u.(F.(d1,d2)) = F.(u.d1,u.d2) by A1,A2,A4,Th60;
end;

theorem Th64:
  F is having_a_unity & F is associative & F is
having_an_inverseOp & (F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d)) implies d1 =
  d2
proof
  assume that
A1: F is having_a_unity and
A2: F is associative and
A3: F is having_an_inverseOp and
A4: F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d);
  set e = the_unity_wrt F, u = the_inverseOp_wrt F;
  per cases by A4;
  suppose
A5: F.(d,d1) = F.(d,d2);
    thus d1 = F.(e,d1) by A1,SETWISEO:15
      .= F.(F.(u.d,d),d1) by A1,A2,A3,Th59
      .= F.(u.d,F.(d,d2)) by A2,A5
      .= F.(F.(u.d,d),d2) by A2
      .= F.(e,d2) by A1,A2,A3,Th59
      .= d2 by A1,SETWISEO:15;
  end;
  suppose
A6: F.(d1,d) = F.(d2,d);
    thus d1 = F.(d1,e) by A1,SETWISEO:15
      .= F.(d1,F.(d,u.d)) by A1,A2,A3,Th59
      .= F.(F.(d2,d),u.d) by A2,A6
      .= F.(d2,F.(d,u.d)) by A2
      .= F.(d2,e) by A1,A2,A3,Th59
      .= d2 by A1,SETWISEO:15;
  end;
end;

theorem Th65:
  F is having_a_unity & F is associative & F is
  having_an_inverseOp & (F.(d1,d2) = d2 or F.(d2,d1) = d2) implies d1 =
  the_unity_wrt F
proof
  assume that
A1: F is having_a_unity and
A2: F is associative & F is having_an_inverseOp;
  set e = the_unity_wrt F;
  assume F.(d1,d2) = d2 or F.(d2,d1) = d2;
  then F.(d1,d2) = F.(e,d2) or F.(d2,d1) = F.(d2,e) by A1,SETWISEO:15;
  hence thesis by A1,A2,Th64;
end;

theorem Th66:
  F is associative & F is having_a_unity & F is
having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F implies for
  d holds G.(e,d) = e & G.(d,e) = e
proof
  assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F and
A5: e = the_unity_wrt F;
  let d;
  set ed = G.(e,d);
  F.(ed,ed) = G.(F.(e,e),d) by A4,BINOP_1:11
    .= ed by A2,A5,SETWISEO:15;
  hence ed = e by A1,A2,A3,A5,Th65;
  set de = G.(d,e);
  F.(de,de) = G.(d,F.(e,e)) by A4,BINOP_1:11
    .= de by A2,A5,SETWISEO:15;
  hence thesis by A1,A2,A3,A5,Th65;
end;

theorem Th67:
  F is having_a_unity & F is associative & F is
having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F implies
  u.(G.(d1,d2)) = G.(u.d1,d2) & u.(G.(d1,d2)) = G.(d1,u.d2)
proof
  assume that
A1: F is having_a_unity & F is associative & F is having_an_inverseOp and
A2: u = the_inverseOp_wrt F and
A3: G is_distributive_wrt F;
  set e = the_unity_wrt F;
  F.(G.(d1,d2),G.(u.d1,d2)) = G.(F.(d1,u.d1),d2) by A3,BINOP_1:11
    .= G.(e,d2) by A1,A2,Th59
    .= e by A1,A3,Th66;
  hence u.(G.(d1,d2)) = G.(u.d1,d2) by A1,A2,Th60;
  F.(G.(d1,d2),G.(d1,u.d2)) = G.(d1,F.(d2,u.d2)) by A3,BINOP_1:11
    .= G.(d1,e) by A1,A2,Th59
    .= e by A1,A3,Th66;
  hence thesis by A1,A2,Th60;
end;

theorem
  F is having_a_unity & F is associative & F is having_an_inverseOp & u
= the_inverseOp_wrt F & G is_distributive_wrt F & G is having_a_unity implies G
  [;](u.(the_unity_wrt G),id D) = u
proof
  assume that
A1: F is having_a_unity & F is associative & F is having_an_inverseOp &
  u = the_inverseOp_wrt F & G is_distributive_wrt F and
A2: G is having_a_unity;
  set o = the_unity_wrt G;
  for d holds (G[;](u.o,id D)).d = u.d
  proof
    let d;
    thus (G[;](u.o,id D)).d = G.(u.o,(id D).d) by FUNCOP_1:53
      .= G.(u.o,d)
      .= u.(G.(o,d)) by A1,Th67
      .= u.d by A2,SETWISEO:15;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  F is associative & F is having_a_unity & F is having_an_inverseOp & G
  is_distributive_wrt F implies G[;](d,id D).the_unity_wrt F = the_unity_wrt F
proof
  assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F;
  set e = the_unity_wrt F, i = the_inverseOp_wrt F;
  G.(d,e) = G.(d,F.(e,e)) by A2,SETWISEO:15
    .= F.(G.(d,e),G.(d,e)) by A4,BINOP_1:11;
  then e = F.(F.(G.(d,e),G.(d,e)),i.(G.(d,e))) by A1,A2,A3,Th59;
  then e = F.(G.(d,e),F.(G.(d,e),i.(G.(d,e)))) by A1;
  then e = F.(G.(d,e),e) by A1,A2,A3,Th59;
  then e = G.(d,e) by A2,SETWISEO:15;
  then G.(d,(id D).e) = e;
  hence thesis by FUNCOP_1:53;
end;

theorem
  F is associative & F is having_a_unity & F is having_an_inverseOp & G
  is_distributive_wrt F implies G[:](id D,d).the_unity_wrt F = the_unity_wrt F
proof
  assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F;
  set e = the_unity_wrt F, i = the_inverseOp_wrt F;
  G.(e,d) = G.(F.(e,e),d) by A2,SETWISEO:15
    .= F.(G.(e,d),G.(e,d)) by A4,BINOP_1:11;
  then e = F.(F.(G.(e,d),G.(e,d)),i.(G.(e,d))) by A1,A2,A3,Th59;
  then e = F.(G.(e,d),F.(G.(e,d),i.(G.(e,d)))) by A1;
  then e = F.(G.(e,d),e) by A1,A2,A3,Th59;
  then e = G.(e,d) by A2,SETWISEO:15;
  then G.((id D).e,d) = e;
  hence thesis by FUNCOP_1:48;
end;

theorem Th71:
  F is having_a_unity & F is associative & F is
having_an_inverseOp implies F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt
  F & F.:((the_inverseOp_wrt F)*f,f) = C-->the_unity_wrt F
proof
  set u = the_inverseOp_wrt F;
  reconsider g = C-->the_unity_wrt F as Function of C,D;
  assume
A1: F is having_a_unity & F is associative & F is having_an_inverseOp;
  now
    let c;
    thus (F.:(f,u*f)).c = F.(f.c,(u*f).c) by FUNCOP_1:37
      .= F.(f.c,u.(f.c)) by FUNCT_2:15
      .= the_unity_wrt F by A1,Th59
      .= g.c;
  end;
  hence F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt F by FUNCT_2:63;
  now
    let c;
    thus (F.:(u*f,f)).c = F.((u*f).c,f.c) by FUNCOP_1:37
      .= F.(u.(f.c),f.c) by FUNCT_2:15
      .= the_unity_wrt F by A1,Th59
      .= g.c;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th72:
  F is associative & F is having_an_inverseOp & F is
having_a_unity & F.:(f,f9) = C-->the_unity_wrt F implies f = (the_inverseOp_wrt
  F)*f9 & (the_inverseOp_wrt F)*f = f9
proof
  assume that
A1: F is associative & F is having_an_inverseOp & F is having_a_unity and
A2: F.:(f,f9) = C-->the_unity_wrt F;
  set u = the_inverseOp_wrt F;
  set e = the_unity_wrt F;
  reconsider g = C-->e as Function of C,D;
  now
    let c;
    F.(f.c,f9.c) = g.c by A2,FUNCOP_1:37
      .= e;
    hence f.c = u.(f9.c) by A1,Th60
      .= (u*f9).c by FUNCT_2:15;
  end;
  hence f = (the_inverseOp_wrt F)*f9 by FUNCT_2:63;
  now
    let c;
    F.(f.c,f9.c) = g.c by A2,FUNCOP_1:37
      .= e;
    then f9.c = u.(f.c) by A1,Th60;
    hence (u*f).c = f9.c by FUNCT_2:15;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  F is having_a_unity & F is associative & F is having_an_inverseOp
  implies F.:(T,(the_inverseOp_wrt F)*T) = i|->the_unity_wrt F & F.:((
  the_inverseOp_wrt F)*T,T) = i|->the_unity_wrt F
proof
  assume
A1: F is having_a_unity & F is associative & F is having_an_inverseOp;
  reconsider uT = the_inverseOp_wrt F*T as Element of i-tuples_on D by
FINSEQ_2:113;
  per cases;
  suppose
A2: i = 0;
    then F.:(T,uT) = <*>D & F.:(uT,T) = <*>D by Lm1;
    hence thesis by A2;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th71;
  end;
end;

theorem
  F is associative & F is having_an_inverseOp & F is having_a_unity & F
  .:(T1,T2) = i|->the_unity_wrt F implies T1 = (the_inverseOp_wrt F)*T2 & (
  the_inverseOp_wrt F)*T1 = T2
proof
  assume
A1: F is associative & F is having_an_inverseOp & F is having_a_unity &
  F .:(T1,T2) = i|->the_unity_wrt F;
  per cases;
  suppose
    i = 0;
    then T1 = <*>D & T2 = <*>D;
    hence thesis;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T1 is Function of C,D & T2 is Function of C,D by Lm4;
    hence thesis by A1,Th72;
  end;
end;

theorem Th75:
  F is associative & F is having_a_unity & e = the_unity_wrt F & F
  is having_an_inverseOp & G is_distributive_wrt F implies G[;](e,f) = C-->e
proof
  reconsider g = C-->e as Function of C,D;
  assume
A1: F is associative & F is having_a_unity & e = the_unity_wrt F & F is
  having_an_inverseOp & G is_distributive_wrt F;
  now
    let c;
    thus (G[;](e,f)).c = G.(e,f.c) by FUNCOP_1:53
      .= e by A1,Th66
      .= g.c;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  F is associative & F is having_a_unity & e = the_unity_wrt F & F is
  having_an_inverseOp & G is_distributive_wrt F implies G[;](e,T) = i|->e
proof
  assume
A1: F is associative & F is having_a_unity & e = the_unity_wrt F & F is
  having_an_inverseOp & G is_distributive_wrt F;
  per cases;
  suppose
A2: i = 0;
    then G[;](e,T) = <*>D by Lm2;
    hence thesis by A2;
  end;
  suppose
    i <> 0;
    then reconsider C = Seg i as non empty set;
    T is Function of C,D by Lm4;
    hence thesis by A1,Th75;
  end;
end;

definition
  let F,f,g be Function;
  func F*(f,g) -> Function equals
  F*[:f,g:];
  correctness;
end;

theorem Th77:
  for F,f,g being Function st [x,y] in dom(F*(f,g)) holds (F*(f,g)
  ).(x,y) = F.(f.x,g.y)
proof
  let F,f,g be Function such that
A1: [x,y] in dom(F*(f,g));
  [x,y] in dom [:f,g:] by A1,FUNCT_1:11;
  then [x,y] in [:dom f,dom g:] by FUNCT_3:def 8;
  then [:f,g:].(x,y) = [f.x,g.y] by FUNCT_3:65;
  hence thesis by A1,FUNCT_1:12;
end;

::$CT

theorem Th78:
  for F being Function of [:D,D9:],E, f being Function of C,D, g
  being Function of C9,D9 holds F*(f,g) is Function of [:C,C9:],E
proof
  let F be Function of [:D,D9:],E, f be Function of C,D, g be Function of C9,
  D9;
  F*(f,g) = F*[:f,g:];
  hence thesis;
end;

theorem
  for u,u9 being Function of D,D holds F*(u,u9) is BinOp of D by Th78;

definition
  let D,F;
  let f,f9 be Function of D,D;
  redefine func F*(f,f9) -> BinOp of D;
  coherence by Th78;
end;

theorem Th80:
  for F being Function of [:D,D9:],E, f being Function of C,D, g
  being Function of C9,D9 holds (F*(f,g)).(c,c9) = F.(f.c,g.c9)
proof
  let F be Function of [:D,D9:],E, f be Function of C,D, g be Function of C9,
  D9;
  set H = F*(f,g);
  H is Function of [:C,C9:],E by Th78;
  then dom H = [:C,C9:] by FUNCT_2:def 1;
  then [c,c9] in dom H by ZFMISC_1:def 2;
  hence thesis by Th77;
end;

theorem Th81:
  for u being Function of D,D holds (F*(id D,u)).(d1,d2) = F.(d1,u
  .d2) & (F*(u,id D)).(d1,d2) = F.(u.d1,d2)
proof
  let u be Function of D,D;
  (id D).d1 = d1 & (id D).d2 = d2;
  hence thesis by Th80;
end;

theorem Th82:
  (F*(id D,u)).:(f,f9) = F.:(f,u*f9)
proof
  now
    let c;
    thus ((F*(id D,u)).:(f,f9)).c = (F*(id D,u)).(f.c,f9.c) by FUNCOP_1:37
      .= F.(f.c,u.(f9.c)) by Th81
      .= F.(f.c,(u*f9).c) by FUNCT_2:15
      .= (F.:(f,u*f9)).c by FUNCOP_1:37;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (F*(id D,u)).:(T1,T2) = F.:(T1,u*T2)
proof
  now
    per cases;
    suppose
      i = 0;
      then (F*(id D,u)).:(T1,T2) = <*>D & u*T2 = <*>D by Lm1;
      hence thesis by FINSEQ_2:73;
    end;
    suppose
      i <> 0;
      then reconsider C = Seg i as non empty set;
      T1 is Function of C,D & T2 is Function of C,D by Lm4;
      hence thesis by Th82;
    end;
  end;
  hence thesis;
end;

theorem
  F is associative & F is having_a_unity & F is commutative & F is
having_an_inverseOp & u = the_inverseOp_wrt F implies u.(F*(id D,u).(d1,d2)) =
  F*(u,id D).(d1,d2) & F*(id D,u).(d1,d2) = u.(F*(u,id D).(d1,d2))
proof
  assume that
A1: F is associative & F is having_a_unity and
A2: F is commutative and
A3: F is having_an_inverseOp & u = the_inverseOp_wrt F;
A4: u is_distributive_wrt F by A1,A2,A3,Th63;
  thus u.(F*(id D,u).(d1,d2)) = u.(F.(d1,u.d2)) by Th81
    .= F.(u.d1,u.(u.d2)) by A4
    .= F.(u.d1,d2) by A1,A3,Th62
    .= F*(u,id D).(d1,d2) by Th81;
  hence thesis by A1,A3,Th62;
end;

theorem
  F is associative & F is having_a_unity & F is having_an_inverseOp
  implies (F*(id D,the_inverseOp_wrt F)).(d,d) = the_unity_wrt F
proof
  assume
A1: F is associative & F is having_a_unity & F is having_an_inverseOp;
  set u = the_inverseOp_wrt F;
  thus F*(id D,u).(d,d) = F.(d,u.d) by Th81
    .= the_unity_wrt F by A1,Th59;
end;

theorem
  F is associative & F is having_a_unity & F is having_an_inverseOp
  implies (F*(id D,the_inverseOp_wrt F)).(d,the_unity_wrt F) = d
proof
  assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp;
  set u = the_inverseOp_wrt F, e = the_unity_wrt F;
  thus (F*(id D,u)).(d,e) = F.(d,u.e) by Th81
    .= F.(d,e) by A1,A2,A3,Th61
    .= d by A2,SETWISEO:15;
end;

theorem
  F is having_a_unity implies (F*(id D,u)).(the_unity_wrt F,d) = u.d
proof
  assume
A1: F is having_a_unity;
  set e = the_unity_wrt F;
  thus (F*(id D,u)).(e,d) = F.(e,u.d) by Th81
    .= u.d by A1,SETWISEO:15;
end;

theorem
  F is commutative & F is associative & F is having_a_unity & F is
having_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies for d1,d2,d3,d4
  holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4))
proof
  assume that
A1: F is commutative and
A2: F is associative and
A3: F is having_a_unity & F is having_an_inverseOp and
A4: G = F*(id D,the_inverseOp_wrt F);
  set u = the_inverseOp_wrt F;
A5: u is_distributive_wrt F by A1,A2,A3,Th63;
  let d1,d2,d3,d4;
  thus F.(G.(d1,d2),G.(d3,d4)) = F.(F.(d1,u.d2),G.(d3,d4)) by A4,Th81
    .= F.(F.(d1,u.d2),F.(d3,u.d4)) by A4,Th81
    .= F.(d1,F.(u.d2,F.(d3,u.d4))) by A2
    .= F.(d1,F.(F.(u.d2,d3),u.d4)) by A2
    .= F.(d1,F.(F.(d3,u.d2),u.d4)) by A1
    .= F.(d1,F.(d3,F.(u.d2,u.d4))) by A2
    .= F.(F.(d1,d3),F.(u.d2,u.d4)) by A2
    .= F.(F.(d1,d3),u.(F.(d2,d4))) by A5
    .= G.(F.(d1,d3),F.(d2,d4)) by A4,Th81;
end;

subset_name: curated