i in INT by INT_1:def 2;
then consider n being Nat such that
A1: ( i = n or i = - n ) by INT_1:def 1;
per cases ( i = n or i = - n ) by A1;
suppose A2: i = n ; :: thesis: ex b1 being Element of R ex n being Nat st
( ( i = n & b1 = n * a ) or ( i = - n & b1 = - (n * a) ) )
take n * a ; :: thesis: ex n being Nat st
( ( i = n & n * a = n * a ) or ( i = - n & n * a = - (n * a) ) )
thus ex n being Nat st
( ( i = n & n * a = n * a ) or ( i = - n & n * a = - (n * a) ) ) by A2; :: thesis: verum
end;
suppose A3: i = - n ; :: thesis: ex b1 being Element of R ex n being Nat st
( ( i = n & b1 = n * a ) or ( i = - n & b1 = - (n * a) ) )
take - (n * a) ; :: thesis: ex n being Nat st
( ( i = n & - (n * a) = n * a ) or ( i = - n & - (n * a) = - (n * a) ) )
thus ex n being Nat st
( ( i = n & - (n * a) = n * a ) or ( i = - n & - (n * a) = - (n * a) ) ) by A3; :: thesis: verum
end;
end;