hereby ( ( for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f) ) implies F is comp-preserving )
assume A1:
F is
comp-preserving
;
for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f)let o1,
o2,
o3 be
Object of
C1;
( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . 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 F . (g * f) = (F . g) * (F . f)let f be
Morphism of
o1,
o2;
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f)let g be
Morphism of
o2,
o3;
F . (g * f) = (F . g) * (F . f)consider f9 being
Morphism of
(F . o1),
(F . o2),
g9 being
Morphism of
(F . o2),
(F . o3) such that A4:
f9 = (Morph-Map (F,o1,o2)) . f
and A5:
g9 = (Morph-Map (F,o2,o3)) . g
and A6:
(Morph-Map (F,o1,o3)) . (g * f) = g9 * f9
by A1, A2, A3;
A7:
<^(F . o1),(F . o2)^> <> {}
by A2, Def18;
A8:
<^(F . o2),(F . o3)^> <> {}
by A3, Def18;
A9:
f9 = F . f
by A2, A4, A7, Def15;
A10:
g9 = F . g
by A3, A5, A8, Def15;
A11:
<^o1,o3^> <> {}
by A2, A3, ALTCAT_1:def 2;
then
<^(F . o1),(F . o3)^> <> {}
by Def18;
hence
F . (g * f) = (F . g) * (F . f)
by A6, A9, A10, A11, Def15;
verum
end;
assume A12:
for o1, o2, o3 being Object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f)
; F is comp-preserving
let o1, o2, o3 be Object of C1; FUNCTOR0:def 21 ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 ) )
assume that
A13:
<^o1,o2^> <> {}
and
A14:
<^o2,o3^> <> {}
; for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 )
let f be Morphism of o1,o2; for g being Morphism of o2,o3 ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 )
let g be Morphism of o2,o3; ex f9 being Morphism of (F . o1),(F . o2) ex g9 being Morphism of (F . o2),(F . o3) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 )
A15:
<^(F . o1),(F . o2)^> <> {}
by A13, Def18;
then reconsider f9 = (Morph-Map (F,o1,o2)) . f as Morphism of (F . o1),(F . o2) by A13, FUNCT_2:5;
A16:
<^(F . o2),(F . o3)^> <> {}
by A14, Def18;
then reconsider g9 = (Morph-Map (F,o2,o3)) . g as Morphism of (F . o2),(F . o3) by A14, FUNCT_2:5;
take
f9
; ex g9 being Morphism of (F . o2),(F . o3) st
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 )
take
g9
; ( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9 )
thus
( f9 = (Morph-Map (F,o1,o2)) . f & g9 = (Morph-Map (F,o2,o3)) . g )
; (Morph-Map (F,o1,o3)) . (g * f) = g9 * f9
A17:
f9 = F . f
by A13, A15, Def15;
A18:
g9 = F . g
by A14, A16, Def15;
A19:
<^o1,o3^> <> {}
by A13, A14, ALTCAT_1:def 2;
then
<^(F . o1),(F . o3)^> <> {}
by Def18;
hence (Morph-Map (F,o1,o3)) . (g * f) =
F . (g * f)
by A19, Def15
.=
g9 * f9
by A12, A13, A14, A17, A18
;
verum