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 16;
then reconsider e = id a as Morphism of a,a by ALTCAT_1:2;

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 16;
then reconsider g = f as Function by A1, Th31;
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