let A, B, C be Category; :: thesis: for F1, F2 being Functor of A,B
for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds G * t = G * t
let F1, F2 be Functor of A,B; :: thesis: for G being Functor of B,C st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds G * t = G * t
let G be Functor of B,C; :: thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds G * t = G * t )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: for t being natural_transformation of F1,F2 holds G * t = G * t
then A2: F1 is_transformable_to F2 by NATTRA_1:def 7;
let t be natural_transformation of F1,F2; :: thesis: G * t = G * t
thus G * t = G * t by A1, ISOCAT_1:def 7
.= G * t by A2, ISOCAT_1:def 5 ; :: thesis: verum