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:87;
the Arrows of C2 . oo =
the Arrows of C2 . (o,o)
.=
<^o,o^>
by ALTCAT_1:def 1
;
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
object ;
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:87;
x =
[oo,(( the Arrows of C1 . (o3,o4)) --> m)]
by A3, ALTCAT_1:def 1
.=
[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
object ;
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:21;
then x =
[[o1,o2],(( the Arrows of C1 . (o1,o2)) --> m)]
by A4
.=
[[o1,o2],(<^o1,o2^> --> m)]
by ALTCAT_1:def 1
;
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 1;
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, Th18;
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