let C1 be non empty AltGraph ; :: thesis: for C2, C3 being non empty reflexive AltGraph
for F being reflexive feasible FunctorStr of C1,C2
for G being FunctorStr of 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 of C1,C2
for G being FunctorStr of 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 of C1,C2; :: thesis: for G being FunctorStr of 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 of 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 4;
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:46
.= [: 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:106;
dom the MorphMap of F = [: the carrier of C1, the carrier of C1:] by PARTFUN1:def 4;
then [o,o] in dom the MorphMap of F by ZFMISC_1:106;
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 24;
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:22
.= Morph-Map (G,(F . o),(F . o)) by Def11 ;
thus Morph-Map ((G * F),o,o) = (( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F) . (o,o) by Def37
.= (Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o)) by A3, A4, PBOOLE:def 24 ; :: thesis: verum