let V be non empty set ; :: thesis: for a being Object of (Ens V) holds id a = id$ (@ a)

let a be Object of (Ens V); :: thesis: 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 ) )

let a be Object of (Ens V); :: thesis: 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

hence
id a = id$ (@ a)
by CAT_1:def 12; :: thesis: verum
let b be Element of (Ens V); :: thesis: ( ( 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 ) :: thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )

let g be Morphism of b,a; :: thesis: 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 ;

:: thesis: verum

end;set p = the Comp of (Ens V);

thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )

proof

assume A6:
Hom (b,a) <> {}
; :: thesis: for f being Morphism of b,a holds ii (*) f = f
assume A3:
Hom (a,b) <> {}
; :: thesis: for g being Morphism of a,b holds g (*) ii = g

let g be Morphism of a,b; :: thesis: 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 ;

:: thesis: verum

end;let g be Morphism of a,b; :: thesis: 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 ;

:: thesis: verum

let g be Morphism of b,a; :: thesis: 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 ;

:: thesis: verum