let C be Cartesian_category; :: thesis: for a, b, c, d, e, s being Object of C
for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds
(f [x] h) * (g [x] k) = (f * g) [x] (h * k)
let a, b, c, d, e, s be Object of C; :: thesis: for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds
(f [x] h) * (g [x] k) = (f * g) [x] (h * k)
let f be Morphism of a,b; :: thesis: for h being Morphism of c,d
for g being Morphism of e,a
for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds
(f [x] h) * (g [x] k) = (f * g) [x] (h * k)
let h be Morphism of c,d; :: thesis: for g being Morphism of e,a
for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds
(f [x] h) * (g [x] k) = (f * g) [x] (h * k)
let g be Morphism of e,a; :: thesis: for k being Morphism of s,c st Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} holds
(f [x] h) * (g [x] k) = (f * g) [x] (h * k)
let k be Morphism of s,c; :: thesis: ( Hom (a,b) <> {} & Hom (c,d) <> {} & Hom (e,a) <> {} & Hom (s,c) <> {} implies (f [x] h) * (g [x] k) = (f * g) [x] (h * k) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (c,d) <> {} and
A3: Hom (e,a) <> {} and
A4: Hom (s,c) <> {} ; :: thesis: (f [x] h) * (g [x] k) = (f * g) [x] (h * k)
A5: Hom ((e [x] s),s) <> {} by Th19;
then A6: Hom ((e [x] s),c) <> {} by A4, CAT_1:24;
A7: Hom ((e [x] s),e) <> {} by Th19;
then f * (g * (pr1 (e,s))) = (f * g) * (pr1 (e,s)) by A1, A3, CAT_1:25;
then A8: (f * g) [x] (h * k) = <:(f * (g * (pr1 (e,s)))),(h * (k * (pr2 (e,s)))):> by A2, A4, A5, CAT_1:25;
Hom ((e [x] s),a) <> {} by A3, A7, CAT_1:24;
hence (f [x] h) * (g [x] k) = (f * g) [x] (h * k) by A1, A2, A6, A8, Th41; :: thesis: verum