set F = C1 --> (idm o);
reconsider G = C1 --> (idm o) as feasible Covariant FunctorStr over C1,C2 ;
A1:
<^o,o^> <> {}
by ALTCAT_2:def 7;
G is comp-preserving
proof
let o1,
o2,
o3 be
Object of
C1;
FUNCTOR0:def 23 ( <^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 that A2:
<^o1,o2^> <> {}
and A3:
<^o2,o3^> <> {}
;
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f)
A4:
<^o1,o3^> <> {}
by A2, A3, ALTCAT_1:def 2;
let f be
Morphism of
o1,
o2;
for g being Morphism of o2,o3 holds G . (g * f) = (G . g) * (G . f)let g be
Morphism of
o2,
o3;
G . (g * f) = (G . g) * (G . f)
A5:
G . g = idm o
by A3, Th25;
A6:
G . f = idm o
by A2, Th25;
A7:
G . o1 = o
by A1, Th21;
A8:
G . o2 = o
by A1, Th21;
A9:
G . o3 = o
by A1, Th21;
thus G . (g * f) =
idm o
by A4, Th25
.=
(G . g) * (G . f)
by A1, A5, A6, A7, A8, A9, ALTCAT_1:20
;
verum
end;
hence
C1 --> (idm o) is comp-preserving
; C1 --> (idm o) is comp-reversing
let o1, o2, o3 be Object of C1; FUNCTOR0:def 24 ( <^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 that
A10:
<^o1,o2^> <> {}
and
A11:
<^o2,o3^> <> {}
; 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)
A12:
<^o1,o3^> <> {}
by A10, A11, ALTCAT_1:def 2;
let f be 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)
let g be Morphism of o2,o3; (C1 --> (idm o)) . (g * f) = ((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
A13:
(C1 --> (idm o)) . g = idm o
by A11, Th26;
A14:
(C1 --> (idm o)) . f = idm o
by A10, Th26;
A15:
(C1 --> (idm o)) . o1 = o
by A1, Th21;
A16:
(C1 --> (idm o)) . o2 = o
by A1, Th21;
A17:
(C1 --> (idm o)) . o3 = o
by A1, Th21;
thus (C1 --> (idm o)) . (g * f) =
idm o
by A12, Th26
.=
((C1 --> (idm o)) . f) * ((C1 --> (idm o)) . g)
by A1, A13, A14, A15, A16, A17, ALTCAT_1:20
; verum