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