:: deftheorem defines (#) FUNCTOR3:def 3 :
for A, B, C being non empty transitive with_units AltCatStr
for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for t being transformation of F1,F2
for s being transformation of G1,G2 holds s (#) t = (s * F2) `*` (G1 * t);