:: deftheorem defines is_transformable_to FUNCTOR2:def 1 :
for A, B being non empty transitive with_units AltCatStr
for F1, F2 being Functor of A,B holds
( F1 is_transformable_to F2 iff for a being Object of A holds <^(F1 . a),(F2 . a)^> <> {} );