consider F being covariant Functor of F₁(),F₂() such that
A7: for a being Object of F₁() holds F . a = F₃(a) and
A8: 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 A1;
consider G being covariant Functor of F₂(),F₁() such that
A9: for a being Object of F₂() holds G . a = F₄(a) and
A10: for a, b being Object of F₂() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F₆(a,b,f) by A2;
take F ; :: according to YELLOW18:def 2 :: thesis: ex G being covariant Functor of F₂(),F₁() st
( G * F, id F₁() are_naturally_equivalent & F * G, id F₂() are_naturally_equivalent )
take G ; :: thesis: ( G * F, id F₁() are_naturally_equivalent & F * G, id F₂() are_naturally_equivalent )
set GF = G * F;
set I = id F₁();
A11: for a being Object of F₁() holds
( F₇(a) in <^((G * F) . a),((id F₁()) . a)^> & <^((id F₁()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F₁()) . a) st f = F₇(a) holds
f is iso ) )

proof

let a be Object of F₁(); :: thesis: ( F₇(a) in <^((G * F) . a),((id F₁()) . a)^> & <^((id F₁()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F₁()) . a) st f = F₇(a) holds
f is iso ) )
A12: (G * F) . a = G . (F . a) by FUNCTOR0:33
.= F₄((F . a)) by A9
.= F₄(F₃(a)) by A7 ;
A13: (id F₁()) . a = a by FUNCTOR0:29;
then A14: F₇(a) in <^((G * F) . a),((id F₁()) . a)^> by A3, A12;
A15: F₇(a) " in <^((id F₁()) . a),((G * F) . a)^> by A3, A12, A13;
F₇(a) is one-to-one by A3, A12;
hence ( F₇(a) in <^((G * F) . a),((id F₁()) . a)^> & <^((id F₁()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F₁()) . a) st f = F₇(a) holds
f is iso ) ) by A14, A15, Th41; :: thesis: verum

end;

A16: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F₁()) . a) st g1 = F₇(a) holds
for g2 being Morphism of ((G * F) . b),((id F₁()) . b) st g2 = F₇(b) holds
g2 * ((G * F) . f) = ((id F₁()) . f) * g1

proof

let a, b be Object of F₁(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F₁()) . a) st g1 = F₇(a) holds
for g2 being Morphism of ((G * F) . b),((id F₁()) . b) st g2 = F₇(b) holds
g2 * ((G * F) . f) = ((id F₁()) . f) * g1 )
assume A17: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F₁()) . a) st g1 = F₇(a) holds
for g2 being Morphism of ((G * F) . b),((id F₁()) . b) st g2 = F₇(b) holds
g2 * ((G * F) . f) = ((id F₁()) . f) * g1
A18: F₇(a) in <^((G * F) . a),((id F₁()) . a)^> by A11;
A19: F₇(b) in <^((G * F) . b),((id F₁()) . b)^> by A11;
reconsider g2 = F₇(b) as Morphism of ((G * F) . b),((id F₁()) . b) by A11;
A20: <^((G * F) . a),((G * F) . b)^> <> {} by A17, FUNCTOR0:def 18;
A21: <^((id F₁()) . a),((id F₁()) . b)^> <> {} by A17, FUNCTOR0:def 18;
let f be Morphism of a,b; :: thesis: for g1 being Morphism of ((G * F) . a),((id F₁()) . a) st g1 = F₇(a) holds
for g2 being Morphism of ((G * F) . b),((id F₁()) . b) st g2 = F₇(b) holds
g2 * ((G * F) . f) = ((id F₁()) . f) * g1
A22: (G * F) . f = G . (F . f) by A17, FUNCTOR3:6;
A23: F₃(a) = F . a by A7;
A24: F₃(b) = F . b by A7;
A25: F₅(a,b,f) = F . f by A8, A17;
<^(F . a),(F . b)^> <> {} by A17, FUNCTOR0:def 18;
then F₆(F₃(a),F₃(b),F₅(a,b,f)) = (G * F) . f by A10, A22, A23, A24, A25;
then g2 * ((G * F) . f) = F₇(b) * F₆(F₃(a),F₃(b),F₅(a,b,f)) by A19, A20, Th36
.= f * F₇(a) by A5, A17
.= ((id F₁()) . f) * F₇(a) by A17, FUNCTOR0:31 ;
hence for g1 being Morphism of ((G * F) . a),((id F₁()) . a) st g1 = F₇(a) holds
for g2 being Morphism of ((G * F) . b),((id F₁()) . b) st g2 = F₇(b) holds
g2 * ((G * F) . f) = ((id F₁()) . f) * g1 by A18, A21, Th36; :: thesis: verum

end;

ex t being natural_equivalence of G * F, id F₁() st
( G * F, id F₁() are_naturally_equivalent & ( for a being Object of F₁() holds t ! a = F₇(a) ) ) from YELLOW18:sch 15(A11, A16);
hence G * F, id F₁() are_naturally_equivalent ; :: thesis: F * G, id F₂() are_naturally_equivalent
set I = id F₂();
set FG = F * G;
A26: for a being Object of F₂() holds
( F₈(a) in <^((id F₂()) . a),((F * G) . a)^> & <^((F * G) . a),((id F₂()) . a)^> <> {} & ( for f being Morphism of ((id F₂()) . a),((F * G) . a) st f = F₈(a) holds
f is iso ) )

proof

let a be Object of F₂(); :: thesis: ( F₈(a) in <^((id F₂()) . a),((F * G) . a)^> & <^((F * G) . a),((id F₂()) . a)^> <> {} & ( for f being Morphism of ((id F₂()) . a),((F * G) . a) st f = F₈(a) holds
f is iso ) )
A27: (F * G) . a = F . (G . a) by FUNCTOR0:33
.= F₃((G . a)) by A7
.= F₃(F₄(a)) by A9 ;
A28: (id F₂()) . a = a by FUNCTOR0:29;
then A29: F₈(a) in <^((id F₂()) . a),((F * G) . a)^> by A4, A27;
A30: F₈(a) " in <^((F * G) . a),((id F₂()) . a)^> by A4, A27, A28;
F₈(a) is one-to-one by A4, A27;
hence ( F₈(a) in <^((id F₂()) . a),((F * G) . a)^> & <^((F * G) . a),((id F₂()) . a)^> <> {} & ( for f being Morphism of ((id F₂()) . a),((F * G) . a) st f = F₈(a) holds
f is iso ) ) by A29, A30, Th41; :: thesis: verum

end;

A31: for a, b being Object of F₂() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of ((id F₂()) . a),((F * G) . a) st g1 = F₈(a) holds
for g2 being Morphism of ((id F₂()) . b),((F * G) . b) st g2 = F₈(b) holds
g2 * ((id F₂()) . f) = ((F * G) . f) * g1

proof

let a, b be Object of F₂(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b
for g1 being Morphism of ((id F₂()) . a),((F * G) . a) st g1 = F₈(a) holds
for g2 being Morphism of ((id F₂()) . b),((F * G) . b) st g2 = F₈(b) holds
g2 * ((id F₂()) . f) = ((F * G) . f) * g1 )
assume A32: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b
for g1 being Morphism of ((id F₂()) . a),((F * G) . a) st g1 = F₈(a) holds
for g2 being Morphism of ((id F₂()) . b),((F * G) . b) st g2 = F₈(b) holds
g2 * ((id F₂()) . f) = ((F * G) . f) * g1
A33: F₈(a) in <^((id F₂()) . a),((F * G) . a)^> by A26;
reconsider g1 = F₈(a) as Morphism of ((id F₂()) . a),((F * G) . a) by A26;
A34: F₈(b) in <^((id F₂()) . b),((F * G) . b)^> by A26;
A35: <^((F * G) . a),((F * G) . b)^> <> {} by A32, FUNCTOR0:def 18;
A36: <^((id F₂()) . a),((id F₂()) . b)^> <> {} by A32, FUNCTOR0:def 18;
let f be Morphism of a,b; :: thesis: for g1 being Morphism of ((id F₂()) . a),((F * G) . a) st g1 = F₈(a) holds
for g2 being Morphism of ((id F₂()) . b),((F * G) . b) st g2 = F₈(b) holds
g2 * ((id F₂()) . f) = ((F * G) . f) * g1
A37: (F * G) . f = F . (G . f) by A32, FUNCTOR3:6;
A38: F₄(a) = G . a by A9;
A39: F₄(b) = G . b by A9;
A40: F₆(a,b,f) = G . f by A10, A32;
<^(G . a),(G . b)^> <> {} by A32, FUNCTOR0:def 18;
then F₅(F₄(a),F₄(b),F₆(a,b,f)) = (F * G) . f by A8, A37, A38, A39, A40;
then ((F * G) . f) * g1 = F₅(F₄(a),F₄(b),F₆(a,b,f)) * F₈(a) by A33, A35, Th36
.= F₈(b) * f by A6, A32
.= F₈(b) * ((id F₂()) . f) by A32, FUNCTOR0:31 ;
hence for g1 being Morphism of ((id F₂()) . a),((F * G) . a) st g1 = F₈(a) holds
for g2 being Morphism of ((id F₂()) . b),((F * G) . b) st g2 = F₈(b) holds
g2 * ((id F₂()) . f) = ((F * G) . f) * g1 by A34, A36, Th36; :: thesis: verum

end;

ex t being natural_equivalence of id F₂(),F * G st
( id F₂(),F * G are_naturally_equivalent & ( for a being Object of F₂() holds t ! a = F₈(a) ) ) from YELLOW18:sch 15(A26, A31);
hence F * G, id F₂() are_naturally_equivalent ; :: thesis: verum