let n be Nat; :: thesis: for L being non empty non degenerated well-unital domRing-like doubleLoopStr
for x being Element of L st x <> 0. L holds
x |^ n <> 0. L
let L be non empty non degenerated well-unital domRing-like doubleLoopStr ; :: thesis: for x being Element of L st x <> 0. L holds
x |^ n <> 0. L
let x be Element of L; :: thesis: ( x <> 0. L implies x |^ n <> 0. L )
defpred S₁[ Nat] means x |^ $1 <> 0. L;
assume A1: x <> 0. L ; :: thesis: x |^ n <> 0. L

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then (x |^ n) * x <> 0. L by A1, VECTSP_2:def 1;
hence S₁[n + 1] by GROUP_1:def 7; :: thesis: verum

end;

x |^ 0 = 1_ L by BINOM:8;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2);
hence x |^ n <> 0. L ; :: thesis: verum