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