let V be non empty set ; for a being Object of (Ens V) holds id a = id$ (@ a)
let a be Object of (Ens V); id a = id$ (@ a)
reconsider aa = a as Element of V ;
reconsider ii = id$ aa as Morphism of (Ens V) ;
A1: cod ii =
cod (id$ aa)
by Def10
.=
a
;
A2: dom ii =
dom (id$ aa)
by Def9
.=
a
;
then reconsider ii = ii as Morphism of a,a by A1, CAT_1:4;
for b being Object of (Ens V) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
proof
let b be
Element of
(Ens V);
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
set p = the
Comp of
(Ens V);
thus
(
Hom (
a,
b)
<> {} implies for
g being
Morphism of
a,
b holds
g (*) ii = g )
( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )proof
assume A3:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) ii = g
let g be
Morphism of
a,
b;
g (*) ii = g
reconsider gg =
g as
Element of
Maps V ;
A4:
dom gg =
dom g
by Def9
.=
aa
by A3, CAT_1:5
;
then A5:
cod (id$ aa) = dom gg
;
dom g = a
by A3, CAT_1:5;
then
[g,ii] in dom the
Comp of
(Ens V)
by A1, CAT_1:def 6;
hence g (*) ii =
the
Comp of
(Ens V) . (
g,
ii)
by CAT_1:def 1
.=
gg * (id$ aa)
by A5, Def11
.=
g
by A4, Th14
;
verum
end;
assume A6:
Hom (
b,
a)
<> {}
;
for f being Morphism of b,a holds ii (*) f = f
let g be
Morphism of
b,
a;
ii (*) g = g
reconsider gg =
g as
Element of
Maps V ;
A7:
cod gg =
cod g
by Def10
.=
aa
by A6, CAT_1:5
;
then A8:
dom (id$ aa) = cod gg
;
cod g = a
by A6, CAT_1:5;
then
[ii,g] in dom the
Comp of
(Ens V)
by A2, CAT_1:def 6;
hence ii (*) g =
the
Comp of
(Ens V) . (
ii,
g)
by CAT_1:def 1
.=
(id$ aa) * gg
by A8, Def11
.=
g
by A7, Th14
;
verum
end;
hence
id a = id$ (@ a)
by CAT_1:def 12; verum