let A, B, C be Category; :: thesis: for F1, F2 being Functor of A,B st F1 is_transformable_to F2 holds
for t being transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let F1, F2 be Functor of A,B; :: thesis: ( F1 is_transformable_to F2 implies for t being transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a) )
assume A1: F1 is_transformable_to F2 ; :: thesis: for t being transformation of F1,F2
for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let t be transformation of F1,F2; :: thesis: for G being Functor of B,C
for a being Object of A holds (G * t) . a = G /. (t . a)
let G be Functor of B,C; :: thesis: for a being Object of A holds (G * t) . a = G /. (t . a)
let a be Object of A; :: thesis: (G * t) . a = G /. (t . a)
A2: Hom ((F1 . a),(F2 . a)) <> {} by A1;
thus (G * t) . a = (G * t) . a by A1, Th3, NATTRA_1:def 5
.= (G * t) . a by A1, Def5
.= G . (t . a) by FUNCT_2:15
.= G . (t . a) by A1, NATTRA_1:def 5
.= G /. (t . a) by A2, CAT_3:def 10 ; :: thesis: verum