let n be natural number ; :: thesis: ( n > 0 implies 1_ (INT.Group n) = 0 )
assume A1: n > 0 ; :: thesis: 1_ (INT.Group n) = 0
then reconsider e = 0 as Element of Segm n by NAT_1:45;
A2: INT.Group n = multMagma(# (Segm n),(addint n) #) by A1, Def6;
then 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 by A2;
reconsider A = A as Element of NAT by ORDINAL1:def 13;
A3: A < n by A1, NAT_1:45;
A4: e * h = (0 + A) mod n by A2, Def5
.= h by A3, NAT_D:24 ;
h * e = (A + 0) mod n by A2, Def5
.= h by A3, NAT_D:24 ;
hence ( h * e = h & e * h = h ) by A4; :: thesis: verum

end;

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