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 ALTCAT_1:1;

now

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 = proj1 f
.= a by A1, A2, Th31 ;
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