let C1, C2 be non empty category; :: thesis: for D1, D2 being category
for F1 being Functor of C1,D1
for F2 being Functor of C2,D2
for c1 being morphism of C1
for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds
(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]
let D1, D2 be category; :: thesis: for F1 being Functor of C1,D1
for F2 being Functor of C2,D2
for c1 being morphism of C1
for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds
(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]
let F1 be Functor of C1,D1; :: thesis: for F2 being Functor of C2,D2
for c1 being morphism of C1
for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds
(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]
let F2 be Functor of C2,D2; :: thesis: for c1 being morphism of C1
for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds
(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]
let c1 be morphism of C1; :: thesis: for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds
(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]
let c2 be morphism of C2; :: thesis: ( F1 is covariant & F2 is covariant implies (F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)] )
assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: (F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]
A2: ( not D1 is empty & not D2 is empty ) by A1, CAT_6:31;
A3: F1 [x] F2 is covariant by A1, Def22;
A4: F1 . c1 = F1 . ((pr1 (C1,C2)) . [c1,c2]) by Def23
.= (F1 (*) (pr1 (C1,C2))) . [c1,c2] by A1, CAT_6:34
.= ((pr1 (D1,D2)) (*) (F1 [x] F2)) . [c1,c2] by A1, Def22
.= (pr1 (D1,D2)) . ((F1 [x] F2) . [c1,c2]) by A3, CAT_6:34 ;
F2 . c2 = F2 . ((pr2 (C1,C2)) . [c1,c2]) by Def23
.= (F2 (*) (pr2 (C1,C2))) . [c1,c2] by A1, CAT_6:34
.= ((pr2 (D1,D2)) (*) (F1 [x] F2)) . [c1,c2] by A1, Def22
.= (pr2 (D1,D2)) . ((F1 [x] F2) . [c1,c2]) by A3, CAT_6:34 ;
hence (F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)] by A4, A2, Def23; :: thesis: verum