let C be with_binary_products category; 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; 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; 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; 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; 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; ( 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) <> {}
; ( 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) <> {}
; ( 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) <> {}
; ( not Hom (b2,c2) <> {} or (g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2) )
assume A4:
Hom (b2,c2) <> {}
; (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; verum