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 f' being
Morphism of
(F . o1),
(F . o2),
g' being
Morphism of
(F . o2),
(F . o3) 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;
<^(F . o2),(F . o3)^> <> {}
by A3, Def19;
then A8:
(
f' = F . f &
g' = F . g )
by A2, A3, A4, A5, A7, Def16;
A9:
<^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, A8, A9, Def16;
:: 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 . g) * (F . f)
; :: thesis: F is comp-preserving
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 f' being Morphism of (F . o1),(F . o2) ex g' being Morphism of (F . o2),(F . o3) 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
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 . o1),(F . o2) ex g' being Morphism of (F . o2),(F . o3) 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 o1,o2; :: thesis: for g being Morphism of o2,o3 ex f' being Morphism of (F . o1),(F . o2) ex g' being Morphism of (F . o2),(F . o3) 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 o2,o3; :: thesis: ex f' being Morphism of (F . o1),(F . o2) ex g' being Morphism of (F . o2),(F . o3) st
( f' = (Morph-Map F,o1,o2) . f & g' = (Morph-Map F,o2,o3) . g & (Morph-Map F,o1,o3) . (g * f) = g' * f' )
A13:
<^(F . o1),(F . o2)^> <> {}
by A11, Def19;
then reconsider f' = (Morph-Map F,o1,o2) . f as Morphism of (F . o1),(F . o2) by A11, FUNCT_2:7;
A14:
<^(F . o2),(F . o3)^> <> {}
by A12, Def19;
then reconsider g' = (Morph-Map F,o2,o3) . g as Morphism of (F . o2),(F . o3) by A12, FUNCT_2:7;
take
f'
; :: thesis: ex g' being Morphism of (F . o2),(F . o3) 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'
A15:
( f' = F . f & g' = F . g )
by A11, A12, A13, A14, Def16;
A16:
<^o1,o3^> <> {}
by A11, A12, ALTCAT_1:def 4;
then
<^(F . o1),(F . o3)^> <> {}
by Def19;
hence (Morph-Map F,o1,o3) . (g * f) =
F . (g * f)
by A16, Def16
.=
g' * f'
by A10, A11, A12, A15
;
:: thesis: verum