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_{1}[ Nat] means x |^ $1 <> 0. L;

assume A1: x <> 0. L ; :: thesis: x |^ n <> 0. L

then A3: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A2);

hence x |^ n <> 0. L ; :: thesis: verum

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

assume A1: x <> 0. L ; :: thesis: x |^ n <> 0. L

A2: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

x |^ 0 = 1_ L
by BINOM:8;S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume S_{1}[n]
; :: thesis: S_{1}[n + 1]

then (x |^ n) * x <> 0. L by A1, VECTSP_2:def 1;

hence S_{1}[n + 1]
by GROUP_1:def 7; :: thesis: verum

end;assume S

then (x |^ n) * x <> 0. L by A1, VECTSP_2:def 1;

hence S

then A3: S

for n being Nat holds S

hence x |^ n <> 0. L ; :: thesis: verum