let A be non empty set ; :: thesis: for a being object of holds idm a = id a
let a be object of ; :: thesis: idm a = id a
<^a,a^> = Funcs a,a by ALTCAT_1:def 16;
then reconsider e = id a as Morphism of , by ALTCAT_1:2;

now

let b be object of ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of , holds f * e = f )
assume A1: <^a,b^> <> {} ; :: thesis: for f being Morphism of , holds f * e = f
let f be Morphism of ,; :: thesis: f * e = f
A2: <^a,b^> = Funcs a,b by ALTCAT_1:def 16;
then reconsider g = f as Function ;
A3: dom g = proj1 f
.= a by A1, A2, Th31 ;
thus f * e = g * (id a) by A1, ALTCAT_1:def 14
.= f by A3, RELAT_1:78 ; :: thesis: verum

end;

hence idm a = id a by ALTCAT_1:def 19; :: thesis: verum