let A be non empty set ; :: thesis: for a being Object of (EnsCat A) holds idm a = id a
let a be Object of (EnsCat A); :: thesis: idm a = id a
<^a,a^> = Funcs (a,a) by ALTCAT_1:def 14;
then reconsider e = id a as Morphism of a,a by FUNCT_2:126;

now :: thesis: for b being Object of (EnsCat A) st <^a,b^> <> {} holds
for f being Morphism of a,b holds f * e = f

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

end;

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