set I1 = [:the carrier of C1,the carrier of C1:];
set I2 = [:the carrier of C2,the carrier of C2:];
set A = the Arrows of C1;
set B = the Arrows of C2;
reconsider oo = [o,o] as Element of [:the carrier of C2,the carrier of C2:] by ZFMISC_1:106;
the Arrows of C2 . oo =
the Arrows of C2 . o,o
.=
<^o,o^>
by ALTCAT_1:def 2
;
then reconsider m = m as Element of the Arrows of C2 . oo ;
reconsider f = [:the carrier of C1,the carrier of C1:] --> oo as Function of [:the carrier of C1,the carrier of C1:],[:the carrier of C2,the carrier of C2:] ;
reconsider f = f as bifunction of the carrier of C1,the carrier of C2 ;
set M = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } ;
A2:
{ [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } = { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum }
proof
thus
{ [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } c= { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum }
XBOOLE_0:def 10 { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum } c= { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } proof
let x be
set ;
TARSKI:def 3 ( not x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } or x in { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum } )
assume
x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum }
;
x in { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum }
then consider o3,
o4 being
object of
C1 such that A3:
x = [[o3,o4],(<^o3,o4^> --> m)]
;
reconsider oo =
[o3,o4] as
Element of
[:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
x =
[oo,((the Arrows of C1 . o3,o4) --> m)]
by A3, ALTCAT_1:def 2
.=
[oo,((the Arrows of C1 . oo) --> m)]
;
hence
x in { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum }
;
verum
end;
let x be
set ;
TARSKI:def 3 ( not x in { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum } or x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } )
assume
x in { [o9,((the Arrows of C1 . o9) --> m)] where o9 is Element of [:the carrier of C1,the carrier of C1:] : verum }
;
x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum }
then consider o9 being
Element of
[:the carrier of C1,the carrier of C1:] such that A4:
x = [o9,((the Arrows of C1 . o9) --> m)]
;
reconsider o1 =
o9 `1 ,
o2 =
o9 `2 as
Element of
C1 by MCART_1:10;
reconsider o1 =
o1,
o2 =
o2 as
object of
C1 ;
o9 = [o1,o2]
by MCART_1:23;
then x =
[[o1,o2],((the Arrows of C1 . o1,o2) --> m)]
by A4
.=
[[o1,o2],(<^o1,o2^> --> m)]
by ALTCAT_1:def 2
;
hence
x in { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum }
;
verum
end;
the Arrows of C2 . o,o <> {}
by A1, ALTCAT_1:def 2;
then reconsider M = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } as MSUnTrans of f,the Arrows of C1,the Arrows of C2 by A2, Th19;
take
FunctorStr(# f,M #)
; ( the ObjectMap of FunctorStr(# f,M #) = [:the carrier of C1,the carrier of C1:] --> [o,o] & the MorphMap of FunctorStr(# f,M #) = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } )
thus
( the ObjectMap of FunctorStr(# f,M #) = [:the carrier of C1,the carrier of C1:] --> [o,o] & the MorphMap of FunctorStr(# f,M #) = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is object of C1 : verum } )
; verum