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 (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 (id B)) = t
let t be natural_transformation of G1,G2; ( G1 is_naturally_transformable_to G2 implies t (#) (id (id B)) = t )
assume A1:
G1 is_naturally_transformable_to G2
; t (#) (id (id B)) = t
then A2:
G1 * (id B) is_naturally_transformable_to G2 * (id B)
by Th20;
thus t (#) (id (id B)) =
(t * (id B)) `*` (id (G1 * (id B)))
by Th31
.=
t * (id B)
by A2, NATTRA_1:24
.=
t
by A1, Th32
; verum