let R be non empty add-cancelable right_zeroed well-unital distributive associative 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
A2: 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] )
A3: a |^ (n + 1) = (a |^ n) * (a |^ 1) by BINOM:10;
assume a |^ n in I ; :: thesis: S₁[n + 1]
hence S₁[n + 1] by A3, Def3; :: thesis: verum

end;

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