let A be non empty set ; for a being Object of (EnsCat A) holds idm a = id a
let a be Object of (EnsCat A); 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 for b being Object of (EnsCat A) st <^a,b^> <> {} holds
for f being Morphism of a,b holds f * e = flet b be
Object of
(EnsCat A);
( <^a,b^> <> {} implies for f being Morphism of a,b holds f * e = f )assume A1:
<^a,b^> <> {}
;
for f being Morphism of a,b holds f * e = flet f be
Morphism of
a,
b;
f * e = fA2:
<^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
;
verum end;
hence
idm a = id a
by ALTCAT_1:def 17; verum