let o1, o2 be object of C1; :: according to FUNCTOR0:def 12 :: thesis: ( <^o1,o2^> <> {} implies the Arrows of C3 . (the ObjectMap of (G * F) . o1,o2) <> {} )
assume A1: <^o1,o2^> <> {} ; :: thesis: 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:106;
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:23;
A4: the ObjectMap of (G * F) . o1,o2 = (the ObjectMap of G * the ObjectMap of F) . [o1,o2] by Def37
.= the ObjectMap of G . p1,p2 by A2, A3, FUNCT_1:23 ;
<^p1,p2^> = the Arrows of C2 . p1,p2 by ALTCAT_1:def 2
.= the Arrows of C2 . (the ObjectMap of F . o1,o2) by MCART_1:23 ;
then <^p1,p2^> <> {} by A1, Def12;
hence the Arrows of C3 . (the ObjectMap of (G * F) . o1,o2) <> {} by A4, Def12; :: thesis: verum