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 S1[ 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 S2[ 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 S2[x,y] & S2[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 & S2[y,x] ) ) from A3: for x, y, z being object st S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be object ; :: thesis: ( S1[x,y] & S1[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 S1[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 ;
hence y = z by ; :: thesis: verum
end;
consider X being set such that
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):] & S1[y,x] ) ) from 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 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;
assume x is strict covariant Functor of A,B ; :: thesis: 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)) <> {}
proof
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 ; :: thesis: verum
end;
A11: for o1, o2 being Object of A st the Arrows of A . (o1,o2) <> {} holds
the Arrows of B . [(F . o1),(F . o2)] <> {}
proof
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 ; :: thesis: verum
end;
y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):]
proof
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) <> {}
proof
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 ;
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 ;
hence the Arrows of B . (f . i) <> {} by ; :: thesis: verum
end;
for i being set st i in [: the carrier of A, the carrier of A:] & the Arrows of A . i <> {} holds
AA . i <> {}
proof
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 ;
hence AA . i <> {} by ; :: thesis: verum
end;
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
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 ;
hence y in [:(Funcs ([: the carrier of A, the carrier of A:],[: the carrier of B, the carrier of B:])),(union XX):] by ; :: thesis: verum
end;
hence x in X by A8; :: thesis: verum