let C be with_binary_products category; :: thesis: for a1, a2, b1, b2, c1, c2 being Object of C
for f1 being Morphism of a1,b1
for f2 being Morphism of a2,b2
for g1 being Morphism of b1,c1
for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds
(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)
let a1, a2, b1, b2, c1, c2 be Object of C; :: thesis: for f1 being Morphism of a1,b1
for f2 being Morphism of a2,b2
for g1 being Morphism of b1,c1
for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds
(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)
let f1 be Morphism of a1,b1; :: thesis: for f2 being Morphism of a2,b2
for g1 being Morphism of b1,c1
for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds
(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)
let f2 be Morphism of a2,b2; :: thesis: for g1 being Morphism of b1,c1
for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds
(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)
let g1 be Morphism of b1,c1; :: thesis: for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds
(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)
let g2 be Morphism of b2,c2; :: thesis: ( Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} implies (g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2) )
assume A1: Hom (a1,b1) <> {} ; :: thesis: ( not Hom (b1,c1) <> {} or not Hom (a2,b2) <> {} or not Hom (b2,c2) <> {} or (g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2) )
assume A2: Hom (b1,c1) <> {} ; :: thesis: ( not Hom (a2,b2) <> {} or not Hom (b2,c2) <> {} or (g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2) )
assume A3: Hom (a2,b2) <> {} ; :: thesis: ( not Hom (b2,c2) <> {} or (g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2) )
assume A4: Hom (b2,c2) <> {} ; :: thesis: (g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)
A5: Hom (a1,c1) <> {} by A1, A2, CAT_7:22;
A6: Hom ((a1 [x] a2),a1) <> {} by Th42;
A7: Hom ((b1 [x] b2),b1) <> {} by Th42;
A8: Hom ((c1 [x] c2),c1) <> {} by Th42;
A9: Hom ((a1 [x] a2),a2) <> {} by Th42;
A10: Hom ((b1 [x] b2),b2) <> {} by Th42;
A11: Hom ((c1 [x] c2),c2) <> {} by Th42;
A12: Hom ((a1 [x] a2),(b1 [x] b2)) <> {} by A1, A3, Th44;
A13: Hom ((b1 [x] b2),(c1 [x] c2)) <> {} by A2, A4, Th44;
A14: Hom (a2,c2) <> {} by A3, A4, CAT_7:22;
A15: (g1 * f1) * (pr1 (a1,a2)) = g1 * (f1 * (pr1 (a1,a2))) by A6, A1, A2, CAT_7:23
.= g1 * ((pr1 (b1,b2)) * (f1 [x] f2)) by A1, A3, Def16
.= (g1 * (pr1 (b1,b2))) * (f1 [x] f2) by A7, A12, A2, CAT_7:23
.= ((pr1 (c1,c2)) * (g1 [x] g2)) * (f1 [x] f2) by A2, A4, Def16
.= (pr1 (c1,c2)) * ((g1 [x] g2) * (f1 [x] f2)) by A12, A13, A8, CAT_7:23 ;
(g2 * f2) * (pr2 (a1,a2)) = g2 * (f2 * (pr2 (a1,a2))) by A9, A3, A4, CAT_7:23
.= g2 * ((pr2 (b1,b2)) * (f1 [x] f2)) by A1, A3, Def16
.= (g2 * (pr2 (b1,b2))) * (f1 [x] f2) by A10, A12, A4, CAT_7:23
.= ((pr2 (c1,c2)) * (g1 [x] g2)) * (f1 [x] f2) by A2, A4, Def16
.= (pr2 (c1,c2)) * ((g1 [x] g2) * (f1 [x] f2)) by A12, A13, A11, CAT_7:23 ;
hence (g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2) by A15, A14, A5, Def16; :: thesis: verum