let R be non empty add-cancelable add-associative right_zeroed distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed right-ideal Subset of R
for a being Element of I
for n being Element of NAT holds n * a in I
let I be non empty add-closed right-ideal Subset of R; :: thesis: for a being Element of I
for n being Element of NAT holds n * a in I
let a be Element of I; :: thesis: for n being Element of NAT holds n * a in I
let n be Element of NAT ; :: thesis: n * a in I
defpred S₁[ Element of NAT ] means $1 * a in I;
0 * a = 0. R by BINOM:13;
then A1: S₁[ 0 ] by Th3;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: n * a in I ; :: thesis: S₁[n + 1]
(n + 1) * a = (1 * a) + (n * a) by BINOM:16
.= a + (n * a) by BINOM:14 ;
hence S₁[n + 1] by A3, Def1; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence n * a in I ; :: thesis: verum