set F = C1 --> (idm o);
reconsider G = C1 --> (idm o) as feasible Covariant FunctorStr of C1,C2 ;
A1:
<^o,o^> <> {}
by ALTCAT_2:def 7;
G is comp-preserving
proof
let o1,
o2,
o3 be
object of
C1;
:: according to FUNCTOR0:def 24 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f) )
assume A2:
(
<^o1,o2^> <> {} &
<^o2,o3^> <> {} )
;
:: thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f)
then A3:
<^o1,o3^> <> {}
by ALTCAT_1:def 4;
let f be
Morphism of
o1,
o2;
:: thesis: for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f)let g be
Morphism of
o2,
o3;
:: thesis: G . (g * f) = (G . g) * (G . f)
A4:
(
G . g = idm o &
G . f = idm o )
by A2, Th26;
A5:
(
G . o1 = o &
G . o2 = o &
G . o3 = o )
by A1, Th22;
thus G . (g * f) =
idm o
by A3, Th26
.=
(G . g) * (G . f)
by A1, A4, A5, ALTCAT_1:24
;
:: thesis: verum
end;
hence
C1 --> (idm o) is comp-preserving
; :: thesis: C1 --> (idm o) is comp-reversing
let o1, o2, o3 be object of C1; :: according to FUNCTOR0:def 25 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g) )
assume A6:
( <^o1,o2^> <> {} & <^o2,o3^> <> {} )
; :: thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
then A7:
<^o1,o3^> <> {}
by ALTCAT_1:def 4;
let f be Morphism of o1,o2; :: thesis: for g being Morphism of o2,o3 holds (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
let g be Morphism of o2,o3; :: thesis: (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
A8:
( (C1 --> (idm o)) . g = idm o & (C1 --> (idm o)) . f = idm o )
by A6, Th27;
A9:
( (C1 --> (idm o)) . o1 = o & (C1 --> (idm o)) . o2 = o & (C1 --> (idm o)) . o3 = o )
by A1, Th22;
thus (C1 --> (idm o)) . (g * f) =
idm o
by A7, Th27
.=
((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
by A1, A8, A9, ALTCAT_1:24
; :: thesis: verum