let A, B, C be Category; :: thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let F1, F2 be Functor of A,B; :: thesis: for G1, G2 being Functor of B,C
for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let G1, G2 be Functor of B,C; :: thesis: for s being natural_transformation of F1,F2
for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let s be natural_transformation of F1,F2; :: thesis: for t being natural_transformation of G1,G2 st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
t (#) s = (G2 * s) `*` (t * F1)
let t be natural_transformation of G1,G2; :: thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies t (#) s = (G2 * s) `*` (t * F1) )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; :: thesis: t (#) s = (G2 * s) `*` (t * F1)
A3: ( G1 * F1 is_naturally_transformable_to G1 * F2 & G1 * F2 is_naturally_transformable_to G2 * F2 ) by A1, A2, Th20;
A4: ( G2 * F1 is_naturally_transformable_to G2 * F2 & G1 * F1 is_naturally_transformable_to G2 * F1 ) by A1, A2, Th20;

now :: thesis: for a being Object of A holds ((t * F2) `*` (G1 * s)) . a = ((G2 * s) `*` (t * F1)) . a

let a be Object of A; :: thesis: ((t * F2) `*` (G1 * s)) . a = ((G2 * s) `*` (t * F1)) . a
A5: ( (G1 * F1) . a = G1 . (F1 . a) & (G1 * F2) . a = G1 . (F2 . a) ) by CAT_1:76;
A6: (G2 * F2) . a = G2 . (F2 . a) by CAT_1:76;
A7: ( (G2 * s) . a = G2 /. (s . a) & (G1 * F1) . a = G1 . (F1 . a) ) by A1, Th21, CAT_1:76;
A8: ( Hom ((F1 . a),(F2 . a)) <> {} & (t * F1) . a = t . (F1 . a) ) by A1, A2, Th22, Th23;
A9: ( (G2 * F1) . a = G2 . (F1 . a) & (G2 * F2) . a = G2 . (F2 . a) ) by CAT_1:76;
( (t * F2) . a = t . (F2 . a) & (G1 * s) . a = G1 /. (s . a) ) by A1, A2, Th21, Th22;
hence ((t * F2) `*` (G1 * s)) . a = (t . (F2 . a)) * (G1 /. (s . a)) by A3, A5, A6, NATTRA_1:25
.= ((G2 * s) . a) * ((t * F1) . a) by A2, A8, A7, A9, NATTRA_1:def 8
.= ((G2 * s) `*` (t * F1)) . a by A4, NATTRA_1:25 ;
:: thesis: verum

end;

hence t (#) s = (G2 * s) `*` (t * F1) by A3, Th24, NATTRA_1:23; :: thesis: verum