let L be non empty non degenerated well-unital unital multLoopStr_0 ; :: thesis: ( L is domRing-like implies for x being Element of L
for i being Nat st (power L) . (x,i) = 0. L holds
x = 0. L )
assume A1: L is domRing-like ; :: thesis: for x being Element of L
for i being Nat st (power L) . (x,i) = 0. L holds
x = 0. L
let x be Element of L; :: thesis: for i being Nat st (power L) . (x,i) = 0. L holds
x = 0. L
defpred S₁[ Nat] means ( (power L) . (x,$1) = 0. L implies x = 0. L );
(power L) . (x,0) = 1_ L by GROUP_1:def 7;
then A2: S₁[ 0 ] ;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
reconsider I = i as Element of NAT by ORDINAL1:def 12;
assume A5: ( (power L) . (x,(i + 1)) = 0. L & x <> 0. L ) ; :: thesis: contradiction
then 0. L = ((power L) . (x,I)) * x by GROUP_1:def 7;
hence contradiction by A4, A5, A1, VECTSP_2:def 1; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence for i being Nat st (power L) . (x,i) = 0. L holds
x = 0. L ; :: thesis: verum