hereby :: thesis: ( ( for o1, o2, o3 being object of st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of ,
for g being Morphism of , 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 st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds F . (g * f) = (F . g) * (F . f)
let o1, o2, o3 be object of ; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of ,
for g being Morphism of , holds F . (g * f) = (F . g) * (F . f) )
assume that
A2: <^o1,o2^> <> {} and
A3: <^o2,o3^> <> {} ; :: thesis: for f being Morphism of ,
for g being Morphism of , holds F . (g * f) = (F . g) * (F . f)
let f be Morphism of ,; :: thesis: for g being Morphism of , holds F . (g * f) = (F . g) * (F . f)
let g be Morphism of ,; :: thesis: F . (g * f) = (F . g) * (F . f)
consider f' being Morphism of ,, g' being Morphism of , such that
A4: f' = (Morph-Map F,o1,o2) . f and
A5: g' = (Morph-Map F,o2,o3) . g and
A6: (Morph-Map F,o1,o3) . (g * f) = g' * f' by A1, A2, A3, Def22;
A7: <^(F . o1),(F . o2)^> <> {} by A2, Def19;
A8: <^(F . o2),(F . o3)^> <> {} by A3, Def19;
A9: f' = F . f by A2, A4, A7, Def16;
A10: g' = F . g by A3, A5, A8, Def16;
A11: <^o1,o3^> <> {} by A2, A3, ALTCAT_1:def 4;
then <^(F . o1),(F . o3)^> <> {} by Def19;
hence F . (g * f) = (F . g) * (F . f) by A6, A9, A10, A11, Def16; :: thesis: verum

end;

assume A12: for o1, o2, o3 being object of st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for f being Morphism of ,
for g being Morphism of , holds F . (g * f) = (F . g) * (F . f) ; :: thesis: F is comp-preserving
let o1, o2, o3 be object of ; :: according to FUNCTOR0:def 22 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of ,
for g being Morphism of , ex f' being Morphism of , ex g' being Morphism of , st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = g' * f' ) )
assume that
A13: <^o1,o2^> <> {} and
A14: <^o2,o3^> <> {} ; :: thesis: for f being Morphism of ,
for g being Morphism of , ex f' being Morphism of , ex g' being Morphism of , st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = g' * f' )
let f be Morphism of ,; :: thesis: for g being Morphism of , ex f' being Morphism of , ex g' being Morphism of , st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = g' * f' )
let g be Morphism of ,; :: thesis: ex f' being Morphism of , ex g' being Morphism of , st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = g' * f' )
A15: <^(F . o1),(F . o2)^> <> {} by A13, Def19;
then reconsider f' = (Morph-Map F,o1,o2) . f as Morphism of , by A13, FUNCT_2:7;
A16: <^(F . o2),(F . o3)^> <> {} by A14, Def19;
then reconsider g' = (Morph-Map F,o2,o3) . g as Morphism of , by A14, FUNCT_2:7;
take f' ; :: thesis: ex g' being Morphism of , st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = g' * f' )
take g' ; :: thesis: ( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = g' * f' )
thus ( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g ) ; :: thesis: (Morph-Map F,o1,o3) . (g * f) = g' * f'
A17: f' = F . f by A13, A15, Def16;
A18: g' = F . g by A14, A16, Def16;
A19: <^o1,o3^> <> {} by A13, A14, ALTCAT_1:def 4;
then <^(F . o1),(F . o3)^> <> {} by Def19;
hence (Morph-Map F,o1,o3) . (g * f) = F . (g * f) by A19, Def16
.= g' * f' by A12, A13, A14, A17, A18 ;
:: thesis: verum