let x1, x2 be Element of R; ( ex n being Nat st
( ( i = n & x1 = n * a ) or ( i = - n & x1 = - (n * a) ) ) & ex n being Nat st
( ( i = n & x2 = n * a ) or ( i = - n & x2 = - (n * a) ) ) implies x1 = x2 )
assume that
A4:
ex n being Nat st
( ( i = n & x1 = n * a ) or ( i = - n & x1 = - (n * a) ) )
and
A5:
ex n being Nat st
( ( i = n & x2 = n * a ) or ( i = - n & x2 = - (n * a) ) )
; x1 = x2
i in INT
by INT_1:def 2;
then consider n being Nat such that
A6:
( i = n or i = - n )
by INT_1:def 1;