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 f' being
Morphism of
(F . o2),
(F . o1),
g' being
Morphism of
(F . o3),
(F . o2) 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) = f' * g'
by A1, A2, A3, Def23;
A7:
<^(F . o2),(F . o1)^> <> {}
by A2, Def20;
<^(F . o3),(F . o2)^> <> {}
by A3, Def20;
then A8:
(
f' = F . f &
g' = F . g )
by A2, A3, A4, A5, A7, Def17;
A9:
<^o1,o3^> <> {}
by A2, A3, ALTCAT_1:def 4;
then
<^(F . o3),(F . o1)^> <> {}
by Def20;
hence
F . (g * f) = (F . f) * (F . g)
by A6, A8, A9, Def17;
:: thesis: verum
end;
assume A10:
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 23 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f' being Morphism of (F . o2),(F . o1) ex g' being Morphism of (F . o3),(F . o2) st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = f' * g' ) )
assume that
A11:
<^o1,o2^> <> {}
and
A12:
<^o2,o3^> <> {}
; :: thesis: for f being Morphism of o1,o2
for g being Morphism of o2,o3 ex f' being Morphism of (F . o2),(F . o1) ex g' being Morphism of (F . o3),(F . o2) st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = f' * g' )
let f be Morphism of o1,o2; :: thesis: for g being Morphism of o2,o3 ex f' being Morphism of (F . o2),(F . o1) ex g' being Morphism of (F . o3),(F . o2) st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = f' * g' )
let g be Morphism of o2,o3; :: thesis: ex f' being Morphism of (F . o2),(F . o1) ex g' being Morphism of (F . o3),(F . o2) st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = f' * g' )
A13:
<^(F . o2),(F . o1)^> <> {}
by A11, Def20;
then reconsider f' = (Morph-Map F,o1,o2) . f as Morphism of (F . o2),(F . o1) by A11, FUNCT_2:7;
A14:
<^(F . o3),(F . o2)^> <> {}
by A12, Def20;
then reconsider g' = (Morph-Map F,o2,o3) . g as Morphism of (F . o3),(F . o2) by A12, FUNCT_2:7;
take
f'
; :: thesis: ex g' being Morphism of (F . o3),(F . o2) st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = f' * g' )
take
g'
; :: thesis: ( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = f' * g' )
thus
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g )
; :: thesis: (Morph-Map F,o1,o3) . (g * f) = f' * g'
A15:
( f' = F . f & g' = F . g )
by A11, A12, A13, A14, Def17;
A16:
<^o1,o3^> <> {}
by A11, A12, ALTCAT_1:def 4;
then
<^(F . o3),(F . o1)^> <> {}
by Def20;
hence (Morph-Map F,o1,o3) . (g * f) =
F . (g * f)
by A16, Def17
.=
f' * g'
by A10, A11, A12, A15
;
:: thesis: verum