let x1, x2 be Element of R; :: thesis: ( 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) ) ) ; :: thesis: 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;

per cases ( n = 0 or n <> 0 ) ;

suppose A7: n = 0 ; :: thesis: x1 = x2

then A8: ( x1 = 0. R or x1 = - (0. R) ) by A6, A4, BINOM:12;
( x2 = 0. R or x2 = - (0. R) ) by A6, A5, A7, BINOM:12;
hence x1 = x2 by A8; :: thesis: verum

end;

suppose A9: n <> 0 ; :: thesis: x1 = x2

per cases ( i = n or i = - n ) by A6;

suppose i = n ; :: thesis: x1 = x2

hence x1 = x2 by A9, A5, A4; :: thesis: verum

end;

suppose i = - n ; :: thesis: x1 = x2

hence x1 = x2 by A5, A9, A4; :: thesis: verum

end;

end;

end;

end;