let A1, A2, B1, B2, C1, C2 be category; :: thesis: for F1 being Functor of A1,B1
for F2 being Functor of A2,B2
for G1 being Functor of B1,C1
for G2 being Functor of B2,C2 st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant holds
(G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)
let F1 be Functor of A1,B1; :: thesis: for F2 being Functor of A2,B2
for G1 being Functor of B1,C1
for G2 being Functor of B2,C2 st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant holds
(G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)
let F2 be Functor of A2,B2; :: thesis: for G1 being Functor of B1,C1
for G2 being Functor of B2,C2 st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant holds
(G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)
let G1 be Functor of B1,C1; :: thesis: for G2 being Functor of B2,C2 st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant holds
(G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)
let G2 be Functor of B2,C2; :: thesis: ( F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant implies (G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2) )
assume A1: F1 is covariant ; :: thesis: ( not G1 is covariant or not F2 is covariant or not G2 is covariant or (G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2) )
assume A2: G1 is covariant ; :: thesis: ( not F2 is covariant or not G2 is covariant or (G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2) )
assume A3: F2 is covariant ; :: thesis: ( not G2 is covariant or (G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2) )
assume A4: G2 is covariant ; :: thesis: (G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)
A5: F1 [x] F2 is covariant by A1, A3, Def22;
A6: G1 [x] G2 is covariant by A2, A4, Def22;
A7: G1 (*) F1 is covariant by A1, A2, CAT_6:35;
A8: G2 (*) F2 is covariant by A3, A4, CAT_6:35;
A9: (G1 [x] G2) (*) (F1 [x] F2) is covariant by A5, A6, CAT_6:35;
A10: (G1 (*) F1) (*) (pr1 (A1,A2)) = G1 (*) (F1 (*) (pr1 (A1,A2))) by A1, A2, CAT_7:10
.= G1 (*) ((pr1 (B1,B2)) (*) (F1 [x] F2)) by A1, A3, Def22
.= (G1 (*) (pr1 (B1,B2))) (*) (F1 [x] F2) by A5, A2, CAT_7:10
.= ((pr1 (C1,C2)) (*) (G1 [x] G2)) (*) (F1 [x] F2) by A2, A4, Def22
.= (pr1 (C1,C2)) (*) ((G1 [x] G2) (*) (F1 [x] F2)) by A5, A6, CAT_7:10 ;
(G2 (*) F2) (*) (pr2 (A1,A2)) = G2 (*) (F2 (*) (pr2 (A1,A2))) by A3, A4, CAT_7:10
.= G2 (*) ((pr2 (B1,B2)) (*) (F1 [x] F2)) by A1, A3, Def22
.= (G2 (*) (pr2 (B1,B2))) (*) (F1 [x] F2) by A5, A4, CAT_7:10
.= ((pr2 (C1,C2)) (*) (G1 [x] G2)) (*) (F1 [x] F2) by A2, A4, Def22
.= (pr2 (C1,C2)) (*) ((G1 [x] G2) (*) (F1 [x] F2)) by A5, A6, CAT_7:10 ;
hence (G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2) by A7, A10, A8, A9, Def22; :: thesis: verum