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

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 ||^ n = the carrier of R by A1, Def2;
thus not S ||^ n is empty by A1, Def2; :: thesis: ( S ||^ n is add-closed & S ||^ n is left-ideal & S ||^ n is right-ideal )
thus S ||^ n is add-closed by A2; :: thesis: ( S ||^ n is left-ideal & S ||^ n is right-ideal )
thus S ||^ n is left-ideal by A2; :: 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; :: thesis: verum

end;

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 Def2;
defpred S₁[ Nat] means ( R in dom f implies f . R is Ideal of R );
A6: S₁[ 0 ] by FINSEQ_3:24;
A7: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume that
A8: S₁[m] and
A9: m + 1 in dom f ; :: thesis: f . (m + 1) is Ideal of R

per cases ( m = 0 or m in dom f ) by A9, TOPREALA:2;

suppose m = 0 ; :: thesis: f . (m + 1) is Ideal of R

hence f . (m + 1) is Ideal of R by A4; :: thesis: verum

end;

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

then A11: f /. m = f . m by PARTFUN1:def 6;
f . (m + 1) = S *' (f /. m) by A5, A9, A10;
hence f . (m + 1) is Ideal of R by A10, A8, A11; :: thesis: verum

end;

end;

end;

A12: for m being Nat holds S₁[m] from NAT_1:sch 2(A6, A7);
0 + 1 <= len f by A3, A4, NAT_1:13;
hence ( not S ||^ n is empty & S ||^ n is add-closed & S ||^ n is left-ideal & S ||^ n is right-ideal ) by A4, A12, FINSEQ_3:25; :: thesis: verum

end;

end;