hereby :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: ( <^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^> <> {} ; :: thesis: 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; :: thesis: for g being Morphism of o2,o3 holds F . (g * f) = (F . g) * (F . f)
let g be Morphism of o2,o3; :: thesis: 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; :: thesis: 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) ; :: thesis: F is comp-preserving
let o1, o2, o3 be Object of C1; :: according to FUNCTOR0:def 21 :: thesis: ( <^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^> <> {} ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: (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 ;
:: thesis: verum