let A, B, C be Category; :: thesis: for F1, F2, F3 being Functor of A,B
for G being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let F1, F2, F3 be Functor of A,B; :: thesis: for G being Functor of B,C
for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let G be Functor of B,C; :: thesis: for s being natural_transformation of F1,F2
for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let s be natural_transformation of F1,F2; :: thesis: for s9 being natural_transformation of F2,F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds
G * (s9 `*` s) = (G * s9) `*` (G * s)
let s9 be natural_transformation of F2,F3; :: thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies G * (s9 `*` s) = (G * s9) `*` (G * s) )
assume A1: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) ; :: thesis: G * (s9 `*` s) = (G * s9) `*` (G * s)
then A2: ( G * F1 is_naturally_transformable_to G * F2 & G * F2 is_naturally_transformable_to G * F3 ) by Th20;
now :: thesis: for a being Object of A holds (G * (s9 `*` s)) . a = ((G * s9) `*` (G * s)) . a
let a be Object of A; :: thesis: (G * (s9 `*` s)) . a = ((G * s9) `*` (G * s)) . a
A3: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76;
A4: G . (F3 . a) = (G * F3) . a by CAT_1:76;
A5: ( Hom ((F1 . a),(F2 . a)) <> {} & Hom ((F2 . a),(F3 . a)) <> {} ) by A1, Th23;
A6: ( G /. (s9 . a) = (G * s9) . a & G /. (s . a) = (G * s) . a ) by A1, Th21;
thus (G * (s9 `*` s)) . a = G /. ((s9 `*` s) . a) by A1, Th21, NATTRA_1:23
.= G /. ((s9 . a) * (s . a)) by A1, NATTRA_1:25
.= (G /. (s9 . a)) * (G /. (s . a)) by A5, NATTRA_1:13
.= ((G * s9) `*` (G * s)) . a by A2, A6, A3, A4, NATTRA_1:25 ; :: thesis: verum
end;
hence G * (s9 `*` s) = (G * s9) `*` (G * s) by A2, Th24, NATTRA_1:23; :: thesis: verum