let C be Cartesian_category; :: thesis: 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; :: 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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 <> {} and
A4: Hom e,c <> {} ; :: thesis: (f [x] h) * <:g,k:> = <:(f * g),(h * k):>
A5: Hom e,(a [x] c) <> {} by A3, A4, Th25;
( Hom (a [x] c),a <> {} & Hom (a [x] c),c <> {} & (pr1 a,c) * <:g,k:> = g & (pr2 a,c) * <:g,k:> = k ) by A3, A4, Def11, Th21;
then ( Hom (a [x] c),b <> {} & Hom (a [x] c),d <> {} & f * g = (f * (pr1 a,c)) * <:g,k:> & h * k = (h * (pr2 a,c)) * <:g,k:> ) by A1, A2, A5, CAT_1:52, CAT_1:54;
hence (f [x] h) * <:g,k:> = <:(f * g),(h * k):> by A5, Th27; :: thesis: verum