theorem :: ISOCAT_1:38

for B, C being Category
for G1, G2 being Functor of B,C
for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t (#) (id (id B)) = t