let R be non empty add-cancelable right_zeroed associative well-unital distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of R
for a being Element of I
for n being Element of NAT st n <> 0 holds
a |^ n in I
let I be non empty right-ideal Subset of R; :: thesis: for a being Element of I
for n being Element of NAT st n <> 0 holds
a |^ n in I
let a be Element of I; :: thesis: for n being Element of NAT st n <> 0 holds
a |^ n in I
let n be Element of NAT ; :: thesis: ( n <> 0 implies a |^ n in I )
defpred S₁[ Nat] means a |^ $1 in I;
assume A1: n <> 0 ; :: thesis: a |^ n in I
a |^ 1 = a by BINOM:8;
then A2: S₁[1] ;
A3: for n being Nat st 1 <= n & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( 1 <= n & S₁[n] implies S₁[n + 1] )
assume 1 <= n ; :: thesis: ( not S₁[n] or S₁[n + 1] )
assume A4: a |^ n in I ; :: thesis: S₁[n + 1]
n in NAT by ORDINAL1:def 13;
then a |^ (n + 1) = (a |^ n) * (a |^ 1) by BINOM:11;
hence S₁[n + 1] by A4, Def3; :: thesis: verum

end;

for n being Nat st 1 <= n holds
S₁[n] from NAT_1:sch 8(A2, A3);
hence a |^ n in I by A1, NAT_1:14; :: thesis: verum