let C, B be Category; :: thesis: 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; :: thesis: 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; :: thesis: ( G1 is_naturally_transformable_to G2 implies t * (id B) = t )
assume A1: G1 is_naturally_transformable_to G2 ; :: thesis: t * (id B) = t
A2: ( G1 * (id B) = G1 & G2 * (id B) = G2 ) by FUNCT_2:23;
then reconsider s = t * (id B) as natural_transformation of G1,G2 ;

now

let b be Object of B; :: thesis: s . b = t . b
thus s . b = t . ((id B) . b) by A1, A2, Th29
.= t . b by CAT_1:118 ; :: thesis: verum

end;

hence t * (id B) = t by A1, Th31; :: thesis: verum