theorem Th2: :: FUNCTOR2:2

for A, B being non empty transitive with_units AltCatStr
for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds
F is_transformable_to F2