let B, C be 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 B) = t
let G1, G2 be Functor of B,C; for t being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
t * (id B) = t
let t be natural_transformation of G1,G2; ( G1 is_naturally_transformable_to G2 implies t * (id B) = t )
assume A1:
G1 is_naturally_transformable_to G2
; t * (id B) = t
A2:
G1 * (id B) = G1
by FUNCT_2:17;
then reconsider s = t * (id B) as natural_transformation of G1,G2 by FUNCT_2:17;
A3:
G2 * (id B) = G2
by FUNCT_2:17;
hence
t * (id B) = t
by A1, Th24; verum