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 b₁ being Element of R ex n being Nat st
( ( i = n & b₁ = n * a ) or ( i = - n & b₁ = - (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 b₁ being Element of R ex n being Nat st
( ( i = n & b₁ = n * a ) or ( i = - n & b₁ = - (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;