theorem Th3: :: FUNCTOR2:3

for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t1, t2 being transformation of F1,F2 st ( for a being Object of A holds t1 ! a = t2 ! a ) holds
t1 = t2