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 S1[ Nat] means $1 * a in I;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
A2: (n + 1) * a = (1 * a) + (n * a) by BINOM:15
.= a + (n * a) by BINOM:13 ;
assume n * a in I ; :: thesis: S1[n + 1]
hence S1[n + 1] by A2, Def1; :: thesis: verum
end;
0 * a = 0. R by BINOM:12;
then A3: S1[ 0 ] by Th3;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A1);
 hence n * a in I ; :: thesis: verum