let n be non zero Nat; :: thesis: 1_ (INT.Group n) = 0
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 )

proof

let h be Element of (INT.Group n); :: thesis: ( h * e = h & e * h = h )
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: verum

end;

hence 1_ (INT.Group n) = 0 by GROUP_1:4; :: thesis: verum