let C be non empty category; :: thesis: 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

proof

let f be morphism of C; :: thesis: ( f is identity implies F . f is identity )
assume A2: f is identity ; :: thesis: F . f is identity
F . f = I0 . f by Def21
.= (id X) . f by STRUCT_0:def 4
.= f ;
hence F . f is identity by A2, Th16, Th18; :: thesis: verum

end;

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) )

proof

let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )
assume A4: f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )
A5: F . f1 = I0 . f1 by Def21
.= (id X) . f1 by STRUCT_0:def 4
.= f1 ;
A6: F . f2 = I0 . f2 by Def21
.= (id X) . f2 by STRUCT_0:def 4
.= f2 ;
hence A7: F . f1 |> F . f2 by A4, A5; :: thesis: F . (f1 (*) f2) = (F . f1) (*) (F . f2)
thus F . (f1 (*) f2) = I0 . (f1 (*) f2) by Def21
.= (id X) . (f1 (*) f2) by STRUCT_0:def 4
.= the composition of C . (f1,f2) by A4, Def3
.= (F . f1) (*) (F . f2) by A5, A6, A7, Def3 ; :: thesis: verum

end;

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

proof

let f be morphism of (alter (Alter C)); :: thesis: ( f is identity implies G . f is identity )
assume A9: f is identity ; :: thesis: G . f is identity
G . f = I0 . f by Def21
.= (id X) . f by STRUCT_0:def 4
.= f ;
hence G . f is identity by A9, Th16, Th18; :: thesis: verum

end;

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) )

proof

let f1, f2 be morphism of (alter (Alter C)); :: thesis: ( f1 |> f2 implies ( G . f1 |> G . f2 & G . (f1 (*) f2) = (G . f1) (*) (G . f2) ) )
assume A11: f1 |> f2 ; :: thesis: ( G . f1 |> G . f2 & G . (f1 (*) f2) = (G . f1) (*) (G . f2) )
A12: G . f1 = I0 . f1 by Def21
.= (id X) . f1 by STRUCT_0:def 4
.= f1 ;
A13: G . f2 = I0 . f2 by Def21
.= (id X) . f2 by STRUCT_0:def 4
.= f2 ;
hence A14: G . f1 |> G . f2 by A11, A12; :: thesis: G . (f1 (*) f2) = (G . f1) (*) (G . f2)
thus G . (f1 (*) f2) = I0 . (f1 (*) f2) by Def21
.= (id X) . (f1 (*) f2) by STRUCT_0:def 4
.= the composition of (alter (Alter C)) . (f1,f2) by A11, Def3
.= (G . f1) (*) (G . f2) by A12, A13, A14, Def3 ; :: thesis: verum

end;

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; :: thesis: verum