let C be Cartesian_category; :: thesis: for c, a, b being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let c, a, b be Object of C; :: thesis: for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let f be Morphism of c,a; :: thesis: for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let g be Morphism of c,b; :: thesis: ( Hom (c,a) <> {} & Hom (c,b) <> {} implies <:f,g:> = (f [x] g) * (Delta c) )
assume that
A1: Hom (c,a) <> {} and
A2: Hom (c,b) <> {} ; :: thesis: <:f,g:> = (f [x] g) * (Delta c)
Hom (c,c) <> {} by CAT_1:56;
hence (f [x] g) * (Delta c) = <:(f * (id c)),(g * (id c)):> by A1, A2, Th43
.= <:f,(g * (id c)):> by A1, CAT_1:58
.= <:f,g:> by A2, CAT_1:58 ;
:: thesis: verum