let C1, C2, C3, C4 be category; :: thesis: for F being Functor of C1,C2
for G being Functor of C2,C3
for H being Functor of C3,C4 st F is covariant & G is covariant & H is covariant holds
H (*) (G (*) F) = (H (*) G) (*) F
let F be Functor of C1,C2; :: thesis: for G being Functor of C2,C3
for H being Functor of C3,C4 st F is covariant & G is covariant & H is covariant holds
H (*) (G (*) F) = (H (*) G) (*) F
let G be Functor of C2,C3; :: thesis: for H being Functor of C3,C4 st F is covariant & G is covariant & H is covariant holds
H (*) (G (*) F) = (H (*) G) (*) F
let H be Functor of C3,C4; :: thesis: ( F is covariant & G is covariant & H is covariant implies H (*) (G (*) F) = (H (*) G) (*) F )
assume A1: F is covariant ; :: thesis: ( not G is covariant or not H is covariant or H (*) (G (*) F) = (H (*) G) (*) F )
assume A2: G is covariant ; :: thesis: ( not H is covariant or H (*) (G (*) F) = (H (*) G) (*) F )
assume A3: H is covariant ; :: thesis: H (*) (G (*) F) = (H (*) G) (*) F
set GF = G (*) F;
set HG = H (*) G;
A4: G (*) F is covariant by A1, A2, CAT_6:35;
A5: H (*) G is covariant by A2, A3, CAT_6:35;
thus H (*) (G (*) F) = (G (*) F) * H by A4, A3, CAT_6:def 27
.= (F * G) * H by A1, A2, CAT_6:def 27
.= F * (G * H) by RELAT_1:36
.= F * (H (*) G) by A2, A3, CAT_6:def 27
.= (H (*) G) (*) F by A5, A1, CAT_6:def 27 ; :: thesis: verum