consider O being Function such that
A5: dom O = the carrier of F₁() and
A6: for x being object st x in the carrier of F₁() holds
O . x = F₃(x) from FUNCT_1:sch 3();
rng O c= the carrier of F₂()

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng O ; :: thesis:
then consider x being object such that
A7: x in dom O and
A8: y = O . x by FUNCT_1:def 3;
reconsider x = x as Object of F₁() by A5, A7;
A9: y = F₃(x) by A6, A8;
F₃(x) is Object of F₂() by A1;
hence y in the carrier of F₂() by A9; :: thesis:

end;

then reconsider O = O as Function of the carrier of F₁(), the carrier of F₂() by A5, FUNCT_2:2;
reconsider OM = ~ [:O,O:] as bifunction of the carrier of F₁(), the carrier of F₂() ;
dom [:O,O:] = [: the carrier of F₁(), the carrier of F₁():] by A5, FUNCT_3:def 8;
then A10: dom OM = [: the carrier of F₁(), the carrier of F₁():] by FUNCT_4:46;
defpred S₁[ object , object , object ] means $1 = F₄(($3 `1),($3 `2),$2);
A11: for i being object st i in [: the carrier of F₁(), the carrier of F₁():] holds
for x being object st x in the Arrows of F₁() . i holds
ex y being object st
( y in ( the Arrows of F₂() * OM) . i & S₁[y,x,i] )

let i be object ; :: thesis:
assume A12: i in [: the carrier of F₁(), the carrier of F₁():] ; :: thesis:
then consider a, b being object such that
A13: a in the carrier of F₁() and
A14: b in the carrier of F₁() and
A15: [a,b] = i by ZFMISC_1:def 2;
reconsider a = a, b = b as Object of F₁() by A13, A14;
let x be object ; :: thesis:
assume A16: x in the Arrows of F₁() . i ; :: thesis:
then reconsider f = x as Morphism of a,b by A15;
take y = F₄(a,b,f); :: thesis:
A17: y in the Arrows of F₂() . (F₃(b),F₃(a)) by A2, A15, A16;
A18: F₃(a) = O . a by A6;
( the Arrows of F₂() * OM) . i = the Arrows of F₂() . (OM . (a,b)) by A10, A12, A15, FUNCT_1:13
.= the Arrows of F₂() . ([:O,O:] . (b,a)) by A10, A12, A15, FUNCT_4:43
.= the Arrows of F₂() . ((O . b),(O . a)) by A5, FUNCT_3:def 8 ;
hence y in ( the Arrows of F₂() * OM) . i by A6, A17, A18; :: thesis:
thus S₁[y,x,i] by A15; :: thesis:

end;

consider M being ManySortedFunction of the Arrows of F₁(), the Arrows of F₂() * OM such that
A19: for i being object st i in [: the carrier of F₁(), the carrier of F₁():] holds
ex f being Function of ( the Arrows of F₁() . i),(( the Arrows of F₂() * OM) . i) st
( f = M . i & ( for x being object st x in the Arrows of F₁() . i holds
S₁[f . x,x,i] ) ) from MSSUBFAM:sch 1(A11);
reconsider M = M as MSUnTrans of OM, the Arrows of F₁(), the Arrows of F₂() by FUNCTOR0:def 4;
FunctorStr(# OM,M #) is Contravariant

end;

then reconsider F = FunctorStr(# OM,M #) as Contravariant FunctorStr over F₁(),F₂() ;

let a be Object of F₁(); :: thesis:
[a,a] in dom OM by A10, ZFMISC_1:def 2;
hence F . a = ([:O,O:] . (a,a)) `1 by FUNCT_4:43
.= [(O . a),(O . a)] `1 by A5, FUNCT_3:def 8
.= O . a
.= F₃(a) by A6 ;
:: thesis:

end;

let o1, o2 be Object of F₁(); :: thesis:
assume A22: <^o1,o2^> <> {} ; :: thesis:
let g be Morphism of o1,o2; :: thesis:
[o1,o2] in [: the carrier of F₁(), the carrier of F₁():] by ZFMISC_1:def 2;
then consider f being Function of ( the Arrows of F₁() . [o1,o2]),(( the Arrows of F₂() * OM) . [o1,o2]) such that
A23: f = M . [o1,o2] and
A24: for x being object st x in the Arrows of F₁() . [o1,o2] holds
f . x = F₄(([o1,o2] `1),([o1,o2] `2),x) by A19;
f . g = F₄(([o1,o2] `1),([o1,o2] `2),g) by A22, A24
.= F₄(o1,([o1,o2] `2),g)
.= F₄(o1,o2,g) ;
hence (Morph-Map (F,o1,o2)) . g = F₄(o1,o2,g) by A23; :: thesis:

end;

let o1, o2 be Object of F₁(); :: according to FUNCTOR0:def 19 :: thesis:
set g = the Morphism of o1,o2;
assume A26: <^o1,o2^> <> {} ; :: thesis:
then (Morph-Map (F,o1,o2)) . the Morphism of o1,o2 = F₄(o1,o2, the Morphism of o1,o2) by A21;
then (Morph-Map (F,o1,o2)) . the Morphism of o1,o2 in the Arrows of F₂() . (F₃(o2),F₃(o1)) by A2, A26;
then (Morph-Map (F,o1,o2)) . the Morphism of o1,o2 in the Arrows of F₂() . ((F . o2),F₃(o1)) by A20;
hence not <^(F . o2),(F . o1)^> = {} by A20; :: thesis:

end;

let o1, o2 be Object of F₁(); :: thesis:
assume A28: <^o1,o2^> <> {} ; :: thesis:
let g be Morphism of o1,o2; :: thesis:
A29: (Morph-Map (F,o1,o2)) . g = F₄(o1,o2,g) by A21, A28;
<^(F . o2),(F . o1)^> <> {} by A25, A28;
hence F . g = F₄(o1,o2,g) by A28, A29, FUNCTOR0:def 16; :: thesis:

end;

let o1, o2, o3 be Object of F₁(); :: according to FUNCTOR0:def 22 :: thesis:
assume that
A31: <^o1,o2^> <> {} and
A32: <^o2,o3^> <> {} ; :: thesis:
let f be Morphism of o1,o2; :: thesis:
let g be Morphism of o2,o3; :: thesis:
set a = O . o1;
set b = O . o2;
set c = O . o3;
A33: O . o1 = F₃(o1) by A6;
A34: O . o2 = F₃(o2) by A6;
A35: O . o3 = F₃(o3) by A6;
reconsider f9 = F₄(o1,o2,f) as Morphism of (O . o2),(O . o1) by A2, A31, A33, A34;
reconsider g9 = F₄(o2,o3,g) as Morphism of (O . o3),(O . o2) by A2, A32, A34, A35;
A36: O . o1 = F . o1 by A20, A33;
A37: O . o2 = F . o2 by A20, A34;
A38: O . o3 = F . o3 by A20, A35;
reconsider ff = f9 as Morphism of (F . o2),(F . o1) by A20, A33, A37;
reconsider gg = g9 as Morphism of (F . o3),(F . o2) by A20, A35, A37;
take ff ; :: thesis:
take gg ; :: thesis:
A39: <^o1,o3^> <> {} by A31, A32, ALTCAT_1:def 2;
F₄(o1,o3,(g * f)) = ff * gg by A3, A31, A32, A33, A34, A35, A36, A37, A38;
hence ( ff = (Morph-Map (F,o1,o2)) . f & gg = (Morph-Map (F,o2,o3)) . g & (Morph-Map (F,o1,o3)) . (g * f) = ff * gg ) by A21, A31, A32, A39; :: thesis:

end;

F is Functor of F₁(),F₂()

let o be Object of F₁(); :: thesis:
A40: F . o = F₃(o) by A20;
thus (Morph-Map (F,o,o)) . (idm o) = F₄(o,o,(idm o)) by A21
.= idm (F . o) by A4, A40 ; :: thesis:

end;

end;

then reconsider F = F as strict contravariant Functor of F₁(),F₂() by A30;
take F ; :: thesis:
thus ( ( for a being Object of F₁() holds F . a = F₃(a) ) & ( for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F₄(a,b,f) ) ) by A20, A27; :: thesis: