set A9 = Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]);

set sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } ;

set f = the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]);

the Arrows of B * the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) in { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } ;

then reconsider sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } as non empty set ;

defpred S_{1}[ object , object ] means ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being MSUnTrans of f, the Arrows of A, the Arrows of B st

( $1 = [f,m] & $2 = FunctorStr(# f,m #) & $2 is covariant Functor of A,B );

defpred S_{2}[ object , object ] means ex AA being ManySortedSet of [: the carrier of A, the carrier of A:] st

( $1 = AA & $2 = Funcs ( the Arrows of A,AA) );

A1: for x, y, z being object st S_{2}[x,y] & S_{2}[x,z] holds

y = z ;

consider XX being set such that

A2: for x being object holds

( x in XX iff ex y being object st

( y in sAA & S_{2}[y,x] ) )
from TARSKI:sch 1(A1);

A3: for x, y, z being object st S_{1}[x,y] & S_{1}[x,z] holds

y = z

A8: for x being object holds

( x in X iff ex y being object st

( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & S_{1}[y,x] ) )
from TARSKI:sch 1(A3);

take X ; :: thesis: for x being object holds

( x in X iff x is strict covariant Functor of A,B )

let x be object ; :: thesis: ( x in X iff x is strict covariant Functor of A,B )

thus ( x in X implies x is strict covariant Functor of A,B ) :: thesis: ( x is strict covariant Functor of A,B implies x in X )

then reconsider F = x as strict covariant Functor of A,B ;

reconsider f = the ObjectMap of F as Covariant bifunction of the carrier of A, the carrier of B by FUNCTOR0:def 12;

reconsider m = the MorphMap of F as MSUnTrans of f, the Arrows of A, the Arrows of B ;

reconsider y = [f,m] as set by TARSKI:1;

A9: for o1, o2 being Object of A st the Arrows of A . (o1,o2) <> {} holds

the Arrows of B . (f . (o1,o2)) <> {}

the Arrows of B . [(F . o1),(F . o2)] <> {}

set sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } ;

set f = the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]);

the Arrows of B * the Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) in { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } ;

then reconsider sAA = { ( the Arrows of B * f) where f is Element of Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) : verum } as non empty set ;

defpred S

( $1 = [f,m] & $2 = FunctorStr(# f,m #) & $2 is covariant Functor of A,B );

defpred S

( $1 = AA & $2 = Funcs ( the Arrows of A,AA) );

A1: for x, y, z being object st S

y = z ;

consider XX being set such that

A2: for x being object holds

( x in XX iff ex y being object st

( y in sAA & S

A3: for x, y, z being object st S

y = z

proof

consider X being set such that
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[x,z] implies y = z )

given f being Covariant bifunction of the carrier of A, the carrier of B, m being MSUnTrans of f, the Arrows of A, the Arrows of B such that A4: x = [f,m] and

A5: y = FunctorStr(# f,m #) and

y is covariant Functor of A,B ; :: thesis: ( not S_{1}[x,z] or y = z )

given f1 being Covariant bifunction of the carrier of A, the carrier of B, m1 being MSUnTrans of f1, the Arrows of A, the Arrows of B such that A6: x = [f1,m1] and

A7: z = FunctorStr(# f1,m1 #) and

z is covariant Functor of A,B ; :: thesis: y = z

f = f1 by A4, A6, XTUPLE_0:1;

hence y = z by A4, A5, A6, A7, XTUPLE_0:1; :: thesis: verum

end;given f being Covariant bifunction of the carrier of A, the carrier of B, m being MSUnTrans of f, the Arrows of A, the Arrows of B such that A4: x = [f,m] and

A5: y = FunctorStr(# f,m #) and

y is covariant Functor of A,B ; :: thesis: ( not S

given f1 being Covariant bifunction of the carrier of A, the carrier of B, m1 being MSUnTrans of f1, the Arrows of A, the Arrows of B such that A6: x = [f1,m1] and

A7: z = FunctorStr(# f1,m1 #) and

z is covariant Functor of A,B ; :: thesis: y = z

f = f1 by A4, A6, XTUPLE_0:1;

hence y = z by A4, A5, A6, A7, XTUPLE_0:1; :: thesis: verum

A8: for x being object holds

( x in X iff ex y being object st

( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & S

take X ; :: thesis: for x being object holds

( x in X iff x is strict covariant Functor of A,B )

let x be object ; :: thesis: ( x in X iff x is strict covariant Functor of A,B )

thus ( x in X implies x is strict covariant Functor of A,B ) :: thesis: ( x is strict covariant Functor of A,B implies x in X )

proof

assume
x is strict covariant Functor of A,B
; :: thesis: x in X
assume
x in X
; :: thesis: x is strict covariant Functor of A,B

then ex y being object st

( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being MSUnTrans of f, the Arrows of A, the Arrows of B st

( y = [f,m] & x = FunctorStr(# f,m #) & x is covariant Functor of A,B ) ) by A8;

hence x is strict covariant Functor of A,B ; :: thesis: verum

end;then ex y being object st

( y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] & ex f being Covariant bifunction of the carrier of A, the carrier of B ex m being MSUnTrans of f, the Arrows of A, the Arrows of B st

( y = [f,m] & x = FunctorStr(# f,m #) & x is covariant Functor of A,B ) ) by A8;

hence x is strict covariant Functor of A,B ; :: thesis: verum

then reconsider F = x as strict covariant Functor of A,B ;

reconsider f = the ObjectMap of F as Covariant bifunction of the carrier of A, the carrier of B by FUNCTOR0:def 12;

reconsider m = the MorphMap of F as MSUnTrans of f, the Arrows of A, the Arrows of B ;

reconsider y = [f,m] as set by TARSKI:1;

A9: for o1, o2 being Object of A st the Arrows of A . (o1,o2) <> {} holds

the Arrows of B . (f . (o1,o2)) <> {}

proof

A11:
for o1, o2 being Object of A st the Arrows of A . (o1,o2) <> {} holds
let o1, o2 be Object of A; :: thesis: ( the Arrows of A . (o1,o2) <> {} implies the Arrows of B . (f . (o1,o2)) <> {} )

assume A10: the Arrows of A . (o1,o2) <> {} ; :: thesis: the Arrows of B . (f . (o1,o2)) <> {}

the Arrows of A . (o1,o2) = <^o1,o2^> ;

hence the Arrows of B . (f . (o1,o2)) <> {} by A10, FUNCTOR0:def 11; :: thesis: verum

end;assume A10: the Arrows of A . (o1,o2) <> {} ; :: thesis: the Arrows of B . (f . (o1,o2)) <> {}

the Arrows of A . (o1,o2) = <^o1,o2^> ;

hence the Arrows of B . (f . (o1,o2)) <> {} by A10, FUNCTOR0:def 11; :: thesis: verum

the Arrows of B . [(F . o1),(F . o2)] <> {}

proof

y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):]
let o1, o2 be Object of A; :: thesis: ( the Arrows of A . (o1,o2) <> {} implies the Arrows of B . [(F . o1),(F . o2)] <> {} )

assume A12: the Arrows of A . (o1,o2) <> {} ; :: thesis: the Arrows of B . [(F . o1),(F . o2)] <> {}

f . (o1,o2) = [(F . o1),(F . o2)] by FUNCTOR0:22;

hence the Arrows of B . [(F . o1),(F . o2)] <> {} by A9, A12; :: thesis: verum

end;assume A12: the Arrows of A . (o1,o2) <> {} ; :: thesis: the Arrows of B . [(F . o1),(F . o2)] <> {}

f . (o1,o2) = [(F . o1),(F . o2)] by FUNCTOR0:22;

hence the Arrows of B . [(F . o1),(F . o2)] <> {} by A9, A12; :: thesis: verum

proof

hence
x in X
by A8; :: thesis: verum
set I = [: the carrier of A, the carrier of A:];

reconsider AA = the Arrows of B * f as ManySortedSet of [: the carrier of A, the carrier of A:] ;

A13: for i being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds

the Arrows of B . (f . i) <> {}

AA . i <> {}

the Arrows of A . i = {} ) ) by FUNCTOR0:def 4;

then A21: m in Funcs ( the Arrows of A,AA) by Def9;

A22: f in Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) by FUNCT_2:8;

then the Arrows of B * f in sAA ;

then Funcs ( the Arrows of A,AA) in XX by A2;

then m in union XX by A21, TARSKI:def 4;

hence y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] by A22, ZFMISC_1:def 2; :: thesis: verum

end;reconsider AA = the Arrows of B * f as ManySortedSet of [: the carrier of A, the carrier of A:] ;

A13: for i being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds

the Arrows of B . (f . i) <> {}

proof

for i being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds
let i be set ; :: thesis: ( i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} implies the Arrows of B . (f . i) <> {} )

assume that

A14: i in [: the carrier of A, the carrier of A:] and

A15: the Arrows of A . i <> {} ; :: thesis: the Arrows of B . (f . i) <> {}

consider o1, o2 being object such that

A16: ( o1 in the carrier of A & o2 in the carrier of A ) and

A17: i = [o1,o2] by A14, ZFMISC_1:def 2;

reconsider a1 = o1, a2 = o2 as Object of A by A16;

A18: the Arrows of B . (f . i) = the Arrows of B . (f . (o1,o2)) by A17

.= the Arrows of B . [(F . a1),(F . a2)] by FUNCTOR0:22 ;

the Arrows of A . (o1,o2) <> {} by A15, A17;

hence the Arrows of B . (f . i) <> {} by A11, A18; :: thesis: verum

end;assume that

A14: i in [: the carrier of A, the carrier of A:] and

A15: the Arrows of A . i <> {} ; :: thesis: the Arrows of B . (f . i) <> {}

consider o1, o2 being object such that

A16: ( o1 in the carrier of A & o2 in the carrier of A ) and

A17: i = [o1,o2] by A14, ZFMISC_1:def 2;

reconsider a1 = o1, a2 = o2 as Object of A by A16;

A18: the Arrows of B . (f . i) = the Arrows of B . (f . (o1,o2)) by A17

.= the Arrows of B . [(F . a1),(F . a2)] by FUNCTOR0:22 ;

the Arrows of A . (o1,o2) <> {} by A15, A17;

hence the Arrows of B . (f . i) <> {} by A11, A18; :: thesis: verum

AA . i <> {}

proof

then
( m is ManySortedFunction of the Arrows of A,AA & ( for i being set st i in [: the carrier of A, the carrier of A:] & AA . i = {} holds
let i be set ; :: thesis: ( i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} implies AA . i <> {} )

assume A19: i in [: the carrier of A, the carrier of A:] ; :: thesis: ( not the Arrows of A . i <> {} or AA . i <> {} )

assume A20: the Arrows of A . i <> {} ; :: thesis: AA . i <> {}

AA . i = the Arrows of B . (f . i) by A19, FUNCT_2:15;

hence AA . i <> {} by A13, A19, A20; :: thesis: verum

end;assume A19: i in [: the carrier of A, the carrier of A:] ; :: thesis: ( not the Arrows of A . i <> {} or AA . i <> {} )

assume A20: the Arrows of A . i <> {} ; :: thesis: AA . i <> {}

AA . i = the Arrows of B . (f . i) by A19, FUNCT_2:15;

hence AA . i <> {} by A13, A19, A20; :: thesis: verum

the Arrows of A . i = {} ) ) by FUNCTOR0:def 4;

then A21: m in Funcs ( the Arrows of A,AA) by Def9;

A22: f in Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:]) by FUNCT_2:8;

then the Arrows of B * f in sAA ;

then Funcs ( the Arrows of A,AA) in XX by A2;

then m in union XX by A21, TARSKI:def 4;

hence y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] by A22, ZFMISC_1:def 2; :: thesis: verum