let A, B, C be Category; for G1, G2 being Functor of B,C st G1 is_naturally_transformable_to G2 holds
for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let G1, G2 be Functor of B,C; ( G1 is_naturally_transformable_to G2 implies for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a) )
assume A1:
G1 is_naturally_transformable_to G2
; for F being Functor of A,B
for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
then A2:
G1 is_transformable_to G2
;
let F be Functor of A,B; for t being natural_transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let t be natural_transformation of G1,G2; for a being Object of A holds (t * F) . a = t . (F . a)
let a be Object of A; (t * F) . a = t . (F . a)
thus (t * F) . a =
(t * F) . a
by A1, Def8
.=
t . (F . a)
by A2, Th18
; verum