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 Th18;
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:23;
then A4:
the
Arrows of
C2 . (the ObjectMap of F . o1,o2) = {}
by A1, A2, A3, FUNCT_1:23;
the
Arrows of
C1 . ii =
the
Arrows of
C1 . o1,
o2
by A1, MCART_1:23
.=
<^o1,o2^>
by ALTCAT_1:def 2
.=
{}
by A4, Def12
;
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 Th20;
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