let C be non empty category; C ~= alter (Alter C)
set D = alter (Alter C);
reconsider X = the carrier of C as set ;
reconsider I0 = id C as Function of X,X ;
A1:
I0 = id X
by STRUCT_0:def 4;
reconsider F = id C as Functor of C,(alter (Alter C)) ;
reconsider G = id C as Functor of (alter (Alter C)),C ;
for f being morphism of C st f is identity holds
F . f is identity
then A3:
F is identity-preserving
;
for f1, f2 being morphism of C st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
then
F is multiplicative
;
then A8:
F is covariant
by A3;
for f being morphism of (alter (Alter C)) st f is identity holds
G . f is identity
then A10:
G is identity-preserving
;
for f1, f2 being morphism of (alter (Alter C)) st f1 |> f2 holds
( G . f1 |> G . f2 & G . (f1 (*) f2) = (G . f1) (*) (G . f2) )
then
G is multiplicative
;
then A15:
G is covariant
by A10;
A16: G (*) F =
F * G
by A8, A15, Def27
.=
id (X /\ X)
by A1, FUNCT_1:22
.=
id C
by STRUCT_0:def 4
;
F (*) G =
G * F
by A8, A15, Def27
.=
id (X /\ X)
by A1, FUNCT_1:22
.=
id (alter (Alter C))
by STRUCT_0:def 4
;
hence
C ~= alter (Alter C)
by A8, A15, A16; verum