let A, B, C be Category; :: thesis: for F being Functor of A,B
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 * F = t (#) (id F)
let F be Functor of A,B; :: 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 * F = t (#) (id F)
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 * F = t (#) (id F)
let t be natural_transformation of G1,G2; :: thesis: ( G1 is_naturally_transformable_to G2 implies t * F = t (#) (id F) )
assume G1 is_naturally_transformable_to G2 ; :: thesis: t * F = t (#) (id F)
then G1 * F is_naturally_transformable_to G2 * F by Th20;
hence t * F = (t * F) `*` (id (G1 * F)) by NATTRA_1:24
.= t (#) (id F) by Th31 ;
:: thesis: verum