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

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