let C1 be non empty AltGraph ; for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let C2, C3 be non empty reflexive AltGraph ; for F being reflexive feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let F be reflexive feasible FunctorStr over C1,C2; for G being FunctorStr over C2,C3
for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let G be FunctorStr over C2,C3; for o being Object of C1 holds Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
let o be Object of C1; Morph-Map ((G * F),o,o) = (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
A1:
dom the MorphMap of G = [: the carrier of C2, the carrier of C2:]
by PARTFUN1:def 2;
rng the ObjectMap of F c= [: the carrier of C2, the carrier of C2:]
;
then dom ( the MorphMap of G * the ObjectMap of F) =
dom the ObjectMap of F
by A1, RELAT_1:27
.=
[: the carrier of C1, the carrier of C1:]
by FUNCT_2:def 1
;
then A2:
[o,o] in dom ( the MorphMap of G * the ObjectMap of F)
by ZFMISC_1:87;
dom the MorphMap of F = [: the carrier of C1, the carrier of C1:]
by PARTFUN1:def 2;
then
[o,o] in dom the MorphMap of F
by ZFMISC_1:87;
then
[o,o] in (dom ( the MorphMap of G * the ObjectMap of F)) /\ (dom the MorphMap of F)
by A2, XBOOLE_0:def 4;
then A3:
[o,o] in dom (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F)
by PBOOLE:def 19;
A4: ( the MorphMap of G * the ObjectMap of F) . [o,o] =
the MorphMap of G . ( the ObjectMap of F . (o,o))
by A2, FUNCT_1:12
.=
Morph-Map (G,(F . o),(F . o))
by Def10
;
thus Morph-Map ((G * F),o,o) =
(( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o)
by Def36
.=
(Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))
by A3, A4, PBOOLE:def 19
; verum