let C be Cartesian_category; :: thesis: for a, b, c 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 a, b, c 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) <> {} ;
hence (f [x] g) * (Delta c) = <:(f * (id c)),(g * (id c)):> by A1, A2, Th41
.= <:f,(g * (id c)):> by A1, CAT_1:29
.= <:f,g:> by A2, CAT_1:29 ;
:: thesis: verum