consider t being ManySortedSet of the carrier of F₁() such that
A3: for a being Element of F₁() holds t . a = F₅(a) from PBOOLE:sch 5();
A4: F₃() is_transformable_to F₄() by A1;

now :: thesis: for a being Object of F₁() holds t . a is Morphism of (F₃() . a),(F₄() . a)

let a be Object of F₁(); :: thesis: t . a is Morphism of (F₃() . a),(F₄() . a)
t . a = F₅(a) by A3;
hence t . a is Morphism of (F₃() . a),(F₄() . a) by A1; :: thesis: verum

end;

then reconsider t = t as transformation of F₃(),F₄() by A4, FUNCTOR2:def 2;

A5: now :: thesis: for a being Object of F₁() holds t ! a = F₅(a)

let a be Object of F₁(); :: thesis: t ! a = F₅(a)
t . a = F₅(a) by A3;
hence t ! a = F₅(a) by A4, FUNCTOR2:def 4; :: thesis: verum

end;

A6: F₃() is_naturally_transformable_to F₄()

proof

thus F₃() is_transformable_to F₄() by A4; :: according to FUNCTOR2:def 6 :: thesis: ex b₁ being transformation of F₃(),F₄() st
for b₂, b₃ being Element of the carrier of F₁() holds
( <^b₂,b₃^> = {} or for b₄ being Element of <^b₂,b₃^> holds (b₁ ! b₃) * (F₃() . b₄) = (F₄() . b₄) * (b₁ ! b₂) )
take t ; :: thesis: for b₁, b₂ being Element of the carrier of F₁() holds
( <^b₁,b₂^> = {} or for b₃ being Element of <^b₁,b₂^> holds (t ! b₂) * (F₃() . b₃) = (F₄() . b₃) * (t ! b₁) )
let a, b be Object of F₁(); :: thesis: ( <^a,b^> = {} or for b₁ being Element of <^a,b^> holds (t ! b) * (F₃() . b₁) = (F₄() . b₁) * (t ! a) )
A7: t ! a = F₅(a) by A5;
t ! b = F₅(b) by A5;
hence ( <^a,b^> = {} or for b₁ being Element of <^a,b^> holds (t ! b) * (F₃() . b₁) = (F₄() . b₁) * (t ! a) ) by A2, A7; :: thesis: verum

end;

now :: thesis: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F₃() . f) = (F₄() . f) * (t ! a)

let a, b be Object of F₁(); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (t ! b) * (F₃() . f) = (F₄() . f) * (t ! a) )
A8: t ! a = F₅(a) by A5;
t ! b = F₅(b) by A5;
hence ( <^a,b^> <> {} implies for f being Morphism of a,b holds (t ! b) * (F₃() . f) = (F₄() . f) * (t ! a) ) by A2, A8; :: thesis: verum

end;

then t is natural_transformation of F₃(),F₄() by A6, FUNCTOR2:def 7;
hence ex t being natural_transformation of F₃(),F₄() st
( F₃() is_naturally_transformable_to F₄() & ( for a being Object of F₁() holds t ! a = F₅(a) ) ) by A5, A6; :: thesis: verum