let A, B, C be Category; :: thesis: for F1, F2 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s
let F1, F2 be Functor of A,B; :: thesis: for G being Functor of B,C
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s
let G be Functor of B,C; :: thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G * s = (id G) (#) s
let s be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 implies G * s = (id G) (#) s )
assume F1 is_naturally_transformable_to F2 ; :: thesis: G * s = (id G) (#) s
then G * F1 is_naturally_transformable_to G * F2 by Th20;
hence G * s = (id (G * F2)) `*` (G * s) by NATTRA_1:24
.= (id G) (#) s by Th30 ;
:: thesis: verum