let A be non empty AltCatStr ; :: thesis: for B, C being non empty reflexive AltCatStr
for F being feasible Covariant FunctorStr of A,B
for G being feasible Covariant FunctorStr of B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let B, C be non empty reflexive AltCatStr ; :: thesis: for F being feasible Covariant FunctorStr of A,B
for G being feasible Covariant FunctorStr of B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let F be feasible Covariant FunctorStr of A,B; :: thesis: for G being feasible Covariant FunctorStr of B,C
for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let G be feasible Covariant FunctorStr of B,C; :: thesis: for o1, o2 being object of A
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let o1, o2 be object of A; :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(G * F) . m = G . (F . m)
let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies (G * F) . m = G . (F . m) )
set I = the carrier of A;
reconsider s = the MorphMap of F . o1,o2 as Function ;
reconsider r = ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . o1,o2 as Function ;
reconsider t = (the MorphMap of G * the ObjectMap of F) . o1,o2 as Function ;
A1: dom ((the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) = (dom (the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F) by PBOOLE:def 24
.= [:the carrier of A,the carrier of A:] /\ (dom the MorphMap of F) by PARTFUN1:def 4
.= [:the carrier of A,the carrier of A:] /\ [:the carrier of A,the carrier of A:] by PARTFUN1:def 4
.= [:the carrier of A,the carrier of A:] ;
A2: dom the ObjectMap of F = [:the carrier of A,the carrier of A:] by FUNCT_2:def 1;
A3: [o1,o2] in [:the carrier of A,the carrier of A:] by ZFMISC_1:def 2;
assume A4: <^o1,o2^> <> {} ; :: thesis: (G * F) . m = G . (F . m)
then A5: <^(F . o1),(F . o2)^> <> {} by FUNCTOR0:def 19;
then A6: dom (Morph-Map F,o1,o2) = <^o1,o2^> by FUNCT_2:def 1;
A7: <^(G . (F . o1)),(G . (F . o2))^> <> {} by A5, FUNCTOR0:def 19;
( (G * F) . o1 = G . (F . o1) & (G * F) . o2 = G . (F . o2) ) by FUNCTOR0:34;
hence (G * F) . m = (Morph-Map (G * F),o1,o2) . m by A4, A7, FUNCTOR0:def 16
.= r . m by FUNCTOR0:def 37
.= (t * s) . m by A1, A3, PBOOLE:def 24
.= t . ((Morph-Map F,o1,o2) . m) by A4, A6, FUNCT_1:23
.= t . (F . m) by A4, A5, FUNCTOR0:def 16
.= (the MorphMap of G . (the ObjectMap of F . o1,o2)) . (F . m) by A2, A3, FUNCT_1:23
.= (Morph-Map G,(F . o1),(F . o2)) . (F . m) by FUNCTOR0:23
.= G . (F . m) by A5, A7, FUNCTOR0:def 16 ;
:: thesis: verum