let A be Category; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (id A) /. f = f
let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (id A) /. f = f )
assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds (id A) /. f = f
let f be Morphism of a,b; :: thesis: (id A) /. f = f
thus (id A) /. f = (id A) . f by A1, CAT_3:def 10
.= f by FUNCT_1:18 ; :: thesis: verum