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