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;

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

hence
P = R
by A6, FUNCTOR2:3; :: thesis: verumlet 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;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