let A be non empty AltCatStr ; for B, C being non empty reflexive AltCatStr
for M being feasible Contravariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over 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 ; for M being feasible Contravariant FunctorStr over A,B
for N being feasible Contravariant FunctorStr over 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 over A,B; for N being feasible Contravariant FunctorStr over 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 over 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 o1, o2 be Object of A; for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(N * M) . m = N . (M . m)
let m be Morphism of o1,o2; ( <^o1,o2^> <> {} implies (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 ;
A1: 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 19
.=
[: the carrier of A, the carrier of A:] /\ (dom the MorphMap of M)
by PARTFUN1:def 2
.=
[: the carrier of A, the carrier of A:] /\ [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2
.=
[: the carrier of A, the carrier of A:]
;
A2:
dom the ObjectMap of M = [: 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^> <> {}
; (N * M) . m = N . (M . m)
then A5:
<^(M . o2),(M . o1)^> <> {}
by FUNCTOR0:def 19;
then A6:
dom (Morph-Map (M,o1,o2)) = <^o1,o2^>
by FUNCT_2:def 1;
A7:
<^(N . (M . o1)),(N . (M . o2))^> <> {}
by A5, FUNCTOR0:def 19;
( (N * M) . o1 = N . (M . o1) & (N * M) . o2 = N . (M . o2) )
by FUNCTOR0:33;
hence (N * M) . m =
(Morph-Map ((N * M),o1,o2)) . m
by A4, A7, FUNCTOR0:def 15
.=
r . m
by FUNCTOR0:def 36
.=
(t * s) . m
by A1, A3, PBOOLE:def 19
.=
t . ((Morph-Map (M,o1,o2)) . m)
by A4, A6, FUNCT_1:13
.=
t . (M . m)
by A4, A5, FUNCTOR0:def 16
.=
( the MorphMap of N . ( the ObjectMap of M . (o1,o2))) . (M . m)
by A2, A3, FUNCT_1:13
.=
(Morph-Map (N,(M . o2),(M . o1))) . (M . m)
by FUNCTOR0:23
.=
N . (M . m)
by A5, A7, FUNCTOR0:def 16
;
verum