let B, C, A be Category; :: thesis: for G1, G2 being Functor of B,C st G1 is_transformable_to G2 holds
for F being Functor of A,B
for t being 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; :: thesis: ( G1 is_transformable_to G2 implies for F being Functor of A,B
for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a) )
assume A1: G1 is_transformable_to G2 ; :: thesis: for F being Functor of A,B
for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let F be Functor of A,B; :: thesis: for t being transformation of G1,G2
for a being Object of A holds (t * F) . a = t . (F . a)
let t be transformation of G1,G2; :: thesis: for a being Object of A holds (t * F) . a = t . (F . a)
let a be Object of A; :: thesis: (t * F) . a = t . (F . a)
thus (t * F) . a = (t * F) . a by A1, Th8, NATTRA_1:def 5
.= (t * (Obj F)) . a by A1, Def6
.= t . ((Obj F) . a) by FUNCT_2:15
.= t . (F . a) by A1, NATTRA_1:def 5 ; :: thesis: verum