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