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 |^ 0 = the carrier of R by Def4;
thus not S |^ n is empty by ; :: 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;
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 S1[ Nat] means ( R in dom f implies f . R is Ideal of R );
A6: S1[ 0 ] by FINSEQ_3:24;
A7: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume that
A8: S1[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 ;
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 S1[m] from NAT_1:sch 2(A6, A7);
0 + 1 <= len f by ;
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 ; :: thesis: verum
end;
end;