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, Def1
.= f by FUNCT_1:35 ; :: thesis: verum