per cases
( n = 0 or ex k being Nat st n = k + 1 )
by NAT_1:6;

end;

suppose A1:
n = 0
; :: thesis: ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )

A2:
S |^ 0 = the carrier of R
by Def4;

thus not S |^ n is empty by A1, Def4; :: thesis: ( S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )

thus S |^ n is add-closed by A2, A1; :: thesis: ( S |^ n is left-ideal & S |^ n is right-ideal )

thus S |^ n is left-ideal by A2, A1; :: thesis: S |^ n is right-ideal

let p, x be Element of R; :: according to IDEAL_1:def 3 :: thesis: ( not x in S |^ n or x * p in S |^ n )

thus ( not x in S |^ n or x * p in S |^ n ) by A2, A1; :: thesis: verum

end;thus not S |^ n is empty by A1, Def4; :: thesis: ( S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )

thus S |^ n is add-closed by A2, A1; :: thesis: ( S |^ n is left-ideal & S |^ n is right-ideal )

thus S |^ n is left-ideal by A2, A1; :: thesis: S |^ n is right-ideal

let p, x be Element of R; :: according to IDEAL_1:def 3 :: thesis: ( not x in S |^ n or x * p in S |^ n )

thus ( not x in S |^ n or x * p in S |^ n ) by A2, A1; :: thesis: verum

suppose A3:
ex k being Nat st n = k + 1
; :: thesis: ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )

then consider f being FinSequence of bool the carrier of R such that

A4: ( S |^ n = f . (len f) & len f = n & f . 1 = S ) and

A5: for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) by Def4;

defpred S_{1}[ Nat] means ( R in dom f implies f . R is Ideal of R );

A6: S_{1}[ 0 ]
by FINSEQ_3:24;

A7: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[m]
from NAT_1:sch 2(A6, A7);

0 + 1 <= len f by A3, A4, NAT_1:13;

then len f in dom f by FINSEQ_3:25;

hence ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal ) by A4, A12; :: thesis: verum

end;A4: ( S |^ n = f . (len f) & len f = n & f . 1 = S ) and

A5: for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) by Def4;

defpred S

A6: S

A7: for m being Nat st S

S

proof

A12:
for m being Nat holds S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume that

A8: S_{1}[m]
and

A9: m + 1 in dom f ; :: thesis: f . (m + 1) is Ideal of R

end;assume that

A8: S

A9: m + 1 in dom f ; :: thesis: f . (m + 1) is Ideal of R

0 + 1 <= len f by A3, A4, NAT_1:13;

then len f in dom f by FINSEQ_3:25;

hence ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal ) by A4, A12; :: thesis: verum