let o1, o2 be Object of C1; FUNCTOR0:def 11 ( <^o1,o2^> <> {} implies the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {} )
assume A1:
<^o1,o2^> <> {}
; the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {}
reconsider p1 = ( the ObjectMap of F . (o1,o2)) `1 , p2 = ( the ObjectMap of F . (o1,o2)) `2 as Element of C2 by MCART_1:10;
reconsider p1 = p1, p2 = p2 as Object of C2 ;
[o1,o2] in [: the carrier of C1, the carrier of C1:]
by ZFMISC_1:87;
then A2:
[o1,o2] in dom the ObjectMap of F
by FUNCT_2:def 1;
A3:
the ObjectMap of F . (o1,o2) = [p1,p2]
by MCART_1:21;
A4: the ObjectMap of (G * F) . (o1,o2) =
( the ObjectMap of G * the ObjectMap of F) . [o1,o2]
by Def36
.=
the ObjectMap of G . (p1,p2)
by A2, A3, FUNCT_1:13
;
<^p1,p2^> =
the Arrows of C2 . (p1,p2)
by ALTCAT_1:def 1
.=
the Arrows of C2 . ( the ObjectMap of F . (o1,o2))
by MCART_1:21
;
then
<^p1,p2^> <> {}
by A1, Def11;
hence
the Arrows of C3 . ( the ObjectMap of (G * F) . (o1,o2)) <> {}
by A4, Def11; verum