let B, A be Category; :: thesis: for F1, F2 being Functor of A,B st F1 is_naturally_transformable_to F2 holds
for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2
let F1, F2 be Functor of A,B; :: thesis: ( F1 is_naturally_transformable_to F2 implies for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2 )
assume F1 is_naturally_transformable_to F2 ; :: thesis: for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2
then F1 is_transformable_to F2 by NATTRA_1:def 7;
hence for t1, t2 being natural_transformation of F1,F2 st ( for a being Object of A holds t1 . a = t2 . a ) holds
t1 = t2 by NATTRA_1:19; :: thesis: verum