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
A4: for a being Object of A holds P . a = (e ! a) " and
A5: for a being Object of A holds R . a = (e ! a) " ; :: thesis: P = R
A6: F2 is_transformable_to F1 by A1;
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 A6, FUNCTOR2:def 4
.= (e ! a) " by A4
.= R . a by A5
.= R ! a by A6, FUNCTOR2:def 4 ; :: thesis: verum
end;
hence P = R by A6, FUNCTOR2:3; :: thesis: verum