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 . f) * (F . g) ) implies F is comp-reversing )

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