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 ;
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); :: 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 )
proof
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 ;
then A5: cod (id\$ aa) = dom gg ;
dom g = a by ;
then [g,ii] in dom the Comp of (Ens V) by ;
hence g (*) ii = the Comp of (Ens V) . (g,ii) by CAT_1:def 1
.= gg * (id\$ aa) by
.= g by ;
:: thesis: verum
end;
assume A6: Hom (b,a) <> {} ; :: thesis: 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 ;
then A8: dom (id\$ aa) = cod gg ;
cod g = a by ;
then [ii,g] in dom the Comp of (Ens V) by ;
hence ii (*) g = the Comp of (Ens V) . (ii,g) by CAT_1:def 1
.= (id\$ aa) * gg by
.= g by ;
:: thesis: verum
end;
hence id a = id\$ (@ a) by CAT_1:def 12; :: thesis: verum