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