consider F being covariant Functor of F1(),F2() such that
A7: for a being object of F1() holds F . a = F3(a) and
A8: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f) by A1;
consider G being covariant Functor of F2(),F1() such that
A9: for a being object of F2() holds G . a = F4(a) and
A10: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) by A2;
take F ; :: according to YELLOW18:def 2 :: thesis: ex G being covariant Functor of F2(),F1() st
( G * F, id F1() are_naturally_equivalent & F * G, id F2() are_naturally_equivalent )
take G ; :: thesis: ( G * F, id F1() are_naturally_equivalent & F * G, id F2() are_naturally_equivalent )
set GF = G * F;
set I = id F1();
A11: for a being object of F1() holds
( F7(a) in <^((G * F) . a),((id F1()) . a)^> & <^((id F1()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F1()) . a) st f = F7(a) holds
f is iso ) )
proof
let a be object of F1(); :: thesis: ( F7(a) in <^((G * F) . a),((id F1()) . a)^> & <^((id F1()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F1()) . a) st f = F7(a) holds
f is iso ) )
A12: (G * F) . a = G . (F . a) by FUNCTOR0:34
.= F4((F . a)) by A9
.= F4(F3(a)) by A7 ;
(id F1()) . a = a by FUNCTOR0:30;
then ( F7(a) in <^((G * F) . a),((id F1()) . a)^> & F7(a) " in <^((id F1()) . a),((G * F) . a)^> & F7(a) is one-to-one ) by A3, A12;
hence ( F7(a) in <^((G * F) . a),((id F1()) . a)^> & <^((id F1()) . a),((G * F) . a)^> <> {} & ( for f being Morphism of ((G * F) . a),((id F1()) . a) st f = F7(a) holds
f is iso ) ) by Th43; :: thesis: verum
end;
A13: for a, b being object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1
proof
let a, b be object of F1(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1 )
assume A14: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b
for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1
A15: F7(a) in <^((G * F) . a),((id F1()) . a)^> by A11;
A16: F7(b) in <^((G * F) . b),((id F1()) . b)^> by A11;
reconsider g2 = F7(b) as Morphism of ((G * F) . b),((id F1()) . b) by A11;
A17: ( <^((G * F) . a),((G * F) . b)^> <> {} & <^((id F1()) . a),((id F1()) . b)^> <> {} ) by A14, FUNCTOR0:def 19;
let f be Morphism of a,b; :: thesis: for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1
A18: (G * F) . f = G . (F . f) by A14, FUNCTOR3:6;
( F3(a) = F . a & F3(b) = F . b & F5(a,b,f) = F . f & <^(F . a),(F . b)^> <> {} ) by A7, A8, A14, FUNCTOR0:def 19;
then F6(F3(a),F3(b),F5(a,b,f)) = (G * F) . f by A10, A18;
then g2 * ((G * F) . f) = F7(b) * F6(F3(a),F3(b),F5(a,b,f)) by A16, A17, Th38
.= f * F7(a) by A5, A14
.= ((id F1()) . f) * F7(a) by A14, FUNCTOR0:32 ;
hence for g1 being Morphism of ((G * F) . a),((id F1()) . a) st g1 = F7(a) holds
for g2 being Morphism of ((G * F) . b),((id F1()) . b) st g2 = F7(b) holds
g2 * ((G * F) . f) = ((id F1()) . f) * g1 by A15, A17, Th38; :: thesis: verum
end;
ex t being natural_equivalence of G * F, id F1() st
( G * F, id F1() are_naturally_equivalent & ( for a being object of F1() holds t ! a = F7(a) ) ) from YELLOW18:sch 15(A11, A13);
 hence G * F, id F1() are_naturally_equivalent ; :: thesis: F * G, id F2() are_naturally_equivalent
set I = id F2();
set FG = F * G;
A19: for a being object of F2() holds
( F8(a) in <^((id F2()) . a),((F * G) . a)^> & <^((F * G) . a),((id F2()) . a)^> <> {} & ( for f being Morphism of ((id F2()) . a),((F * G) . a) st f = F8(a) holds
f is iso ) )
proof
let a be object of F2(); :: thesis: ( F8(a) in <^((id F2()) . a),((F * G) . a)^> & <^((F * G) . a),((id F2()) . a)^> <> {} & ( for f being Morphism of ((id F2()) . a),((F * G) . a) st f = F8(a) holds
f is iso ) )
A20: (F * G) . a = F . (G . a) by FUNCTOR0:34
.= F3((G . a)) by A7
.= F3(F4(a)) by A9 ;
(id F2()) . a = a by FUNCTOR0:30;
then ( F8(a) in <^((id F2()) . a),((F * G) . a)^> & F8(a) " in <^((F * G) . a),((id F2()) . a)^> & F8(a) is one-to-one ) by A4, A20;
hence ( F8(a) in <^((id F2()) . a),((F * G) . a)^> & <^((F * G) . a),((id F2()) . a)^> <> {} & ( for f being Morphism of ((id F2()) . a),((F * G) . a) st f = F8(a) holds
f is iso ) ) by Th43; :: thesis: verum
end;
A21: for a, b being object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1
proof
let a, b be object of F2(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b
for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1 )
assume A22: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b
for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1
A23: F8(a) in <^((id F2()) . a),((F * G) . a)^> by A19;
reconsider g1 = F8(a) as Morphism of ((id F2()) . a),((F * G) . a) by A19;
A24: F8(b) in <^((id F2()) . b),((F * G) . b)^> by A19;
A25: ( <^((F * G) . a),((F * G) . b)^> <> {} & <^((id F2()) . a),((id F2()) . b)^> <> {} ) by A22, FUNCTOR0:def 19;
let f be Morphism of a,b; :: thesis: for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1
A26: (F * G) . f = F . (G . f) by A22, FUNCTOR3:6;
( F4(a) = G . a & F4(b) = G . b & F6(a,b,f) = G . f & <^(G . a),(G . b)^> <> {} ) by A9, A10, A22, FUNCTOR0:def 19;
then F5(F4(a),F4(b),F6(a,b,f)) = (F * G) . f by A8, A26;
then ((F * G) . f) * g1 = F5(F4(a),F4(b),F6(a,b,f)) * F8(a) by A23, A25, Th38
.= F8(b) * f by A6, A22
.= F8(b) * ((id F2()) . f) by A22, FUNCTOR0:32 ;
hence for g1 being Morphism of ((id F2()) . a),((F * G) . a) st g1 = F8(a) holds
for g2 being Morphism of ((id F2()) . b),((F * G) . b) st g2 = F8(b) holds
g2 * ((id F2()) . f) = ((F * G) . f) * g1 by A24, A25, Th38; :: thesis: verum
end;
ex t being natural_equivalence of id F2(),F * G st
( id F2(),F * G are_naturally_equivalent & ( for a being object of F2() holds t ! a = F8(a) ) ) from YELLOW18:sch 15(A19, A21);
 hence F * G, id F2() are_naturally_equivalent ; :: thesis: verum