let n be non zero Nat; :: thesis:
reconsider e = 0 as Element of Segm n by NAT_1:44;
reconsider e = e as Element of (INT.Group n) ;
for h being Element of (INT.Group n) holds
( h * e = h & e * h = h )

let h be Element of (INT.Group n); :: thesis:
reconsider A = h as Element of Segm n ;
reconsider A = A as Element of NAT ;
A1: A < n by NAT_1:44;
A2: e * h = (0 + A) mod n by Def4
.= h by A1, NAT_D:24 ;
h * e = (A + 0) mod n by Def4
.= h by A1, NAT_D:24 ;
hence ( h * e = h & e * h = h ) by A2; :: thesis:

end;