let P, R be natural_equivalence of F2,F1; :: thesis: ( ( for a being object of A holds P . a = (e ! a) " ) & ( for a being object of A holds R . a = (e ! a) " ) implies P = R )
assume that
A3: for a being object of A holds P . a = (e ! a) " and
A4: for a being object of A holds R . a = (e ! a) " ; :: thesis: P = R
A5: F2 is_transformable_to F1 by B1, Def4;

now :: thesis: for a being object of A holds P ! a = R ! a

let a be object of A; :: thesis: P ! a = R ! a
thus P ! a = P . a by A5, FUNCTOR2:def 4
.= (e ! a) " by A3
.= R . a by A4
.= R ! a by A5, FUNCTOR2:def 4 ; :: thesis: verum

end;

hence P = R by A5, FUNCTOR2:3; :: thesis: verum