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