let C1 be non empty AltGraph ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: verum