let C be Cartesian_category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom a,b <> {} holds
<:f,f:> = (Delta b) * f
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom a,b <> {} holds
<:f,f:> = (Delta b) * f
let f be Morphism of a,b; :: thesis: ( Hom a,b <> {} implies <:f,f:> = (Delta b) * f )
assume A1: Hom a,b <> {} ; :: thesis: <:f,f:> = (Delta b) * f
A2: Hom b,b <> {} by CAT_1:56;
(id b) * f = f by A1, CAT_1:57;
hence <:f,f:> = (Delta b) * f by A1, A2, Th27; :: thesis: verum