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 (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 (id B)) = t
let t be natural_transformation of G1,G2; :: thesis: ( G1 is_naturally_transformable_to G2 implies t (#) (id (id B)) = t )
assume A1: G1 is_naturally_transformable_to G2 ; :: thesis: 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 ; :: thesis: verum