reconsider O = the ObjectMap of G * the ObjectMap of F as bifunction of the carrier of C1, the carrier of C3 ;
set I1 = [: the carrier of C1, the carrier of C1:];
reconsider H = the MorphMap of G * the ObjectMap of F as MSUnTrans of O, the Arrows of C2 * the ObjectMap of F, the Arrows of C3 by Th17;
for ii being set st ii in [: the carrier of C1, the carrier of C1:] & ( the Arrows of C2 * the ObjectMap of F) . ii = {} & not the Arrows of C1 . ii = {} holds
( the Arrows of C3 * O) . ii = {}
proof
let ii be
set ;
( ii in [: the carrier of C1, the carrier of C1:] & ( the Arrows of C2 * the ObjectMap of F) . ii = {} & not the Arrows of C1 . ii = {} implies ( the Arrows of C3 * O) . ii = {} )
assume that A1:
ii in [: the carrier of C1, the carrier of C1:]
and A2:
( the Arrows of C2 * the ObjectMap of F) . ii = {}
;
( the Arrows of C1 . ii = {} or ( the Arrows of C3 * O) . ii = {} )
A3:
dom the
ObjectMap of
F = [: the carrier of C1, the carrier of C1:]
by FUNCT_2:def 1;
reconsider o1 =
ii `1 ,
o2 =
ii `2 as
Object of
C1 by A1, MCART_1:10;
ii = [o1,o2]
by A1, MCART_1:21;
then A4:
the
Arrows of
C2 . ( the ObjectMap of F . (o1,o2)) = {}
by A1, A2, A3, FUNCT_1:13;
the
Arrows of
C1 . ii =
the
Arrows of
C1 . (
o1,
o2)
by A1, MCART_1:21
.=
<^o1,o2^>
by ALTCAT_1:def 1
.=
{}
by A4, Def11
;
hence
( the
Arrows of
C1 . ii = {} or
( the Arrows of C3 * O) . ii = {} )
;
verum
end;
then reconsider M = H ** the MorphMap of F as MSUnTrans of O, the Arrows of C1, the Arrows of C3 by Th19;
take
FunctorStr(# O,M #)
; ( the ObjectMap of FunctorStr(# O,M #) = the ObjectMap of G * the ObjectMap of F & the MorphMap of FunctorStr(# O,M #) = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )
thus
( the ObjectMap of FunctorStr(# O,M #) = the ObjectMap of G * the ObjectMap of F & the MorphMap of FunctorStr(# O,M #) = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F )
; verum