theorem :: FUNCTOR3:24

for B, C being non empty transitive with_units AltCatStr
for G1, G2 being covariant Functor of B,C
for q being transformation of G1,G2 st G1 is_transformable_to G2 holds
q (#) (idt (id B)) = q