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