let B, C 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 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;

now :: thesis: for b being Object of B holds s . b = t . b

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

end;

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