A3: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of (F₃() . a),(F₄() . a) st g1 = F₅(a) holds
for g2 being Morphism of (F₃() . b),(F₄() . b) st g2 = F₅(b) holds
g2 * (F₃() . f) = (F₄() . f) * g1 by A2;
A4: for a being Object of F₁() holds F₅(a) in <^(F₃() . a),(F₄() . a)^> by A1;
consider t being natural_transformation of F₃(),F₄() such that
A5: F₃() is_naturally_transformable_to F₄() and
A6: for a being Object of F₁() holds t ! a = F₅(a) from YELLOW18:sch 14(A4, A3);
A7: F₄() is_transformable_to F₃() by A1;
A8: F₃(),F₄() are_naturally_equivalent

proof

thus F₃() is_naturally_transformable_to F₄() by A5; :: according to FUNCTOR3:def 4 :: thesis: ( F₄() is_transformable_to F₃() & ex b₁ being natural_transformation of F₃(),F₄() st
for b₂ being Element of the carrier of F₁() holds b₁ ! b₂ is iso )
thus F₄() is_transformable_to F₃() by A7; :: thesis: ex b₁ being natural_transformation of F₃(),F₄() st
for b₂ being Element of the carrier of F₁() holds b₁ ! b₂ is iso
take t ; :: thesis: for b₁ being Element of the carrier of F₁() holds t ! b₁ is iso
let a be Object of F₁(); :: thesis: t ! a is iso
t ! a = F₅(a) by A6;
hence t ! a is iso by A1; :: thesis: verum

end;

now :: thesis: for a being Object of F₁() holds t ! a is iso

let a be Object of F₁(); :: thesis: t ! a is iso
t ! a = F₅(a) by A6;
hence t ! a is iso by A1; :: thesis: verum

end;

then t is natural_equivalence of F₃(),F₄() by A8, FUNCTOR3:def 5;
hence ex t being natural_equivalence of F₃(),F₄() st
( F₃(),F₄() are_naturally_equivalent & ( for a being Object of F₁() holds t ! a = F₅(a) ) ) by A6, A8; :: thesis: verum