let n be Nat; :: thesis: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr

for a being Element of K st a <> 0. K holds

a |^ n <> 0. K

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K st a <> 0. K holds

a |^ n <> 0. K

let a be Element of K; :: thesis: ( a <> 0. K implies a |^ n <> 0. K )

assume A1: a <> 0. K ; :: thesis: a |^ n <> 0. K

defpred S_{1}[ Nat] means a |^ $1 <> 0. K;

a |^ 0 = 1_ K by GROUP_1:def 7;

then A2: S_{1}[ 0 ]
;

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A2, A3);

hence a |^ n <> 0. K ; :: thesis: verum

for a being Element of K st a <> 0. K holds

a |^ n <> 0. K

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K st a <> 0. K holds

a |^ n <> 0. K

let a be Element of K; :: thesis: ( a <> 0. K implies a |^ n <> 0. K )

assume A1: a <> 0. K ; :: thesis: a |^ n <> 0. K

defpred S

a |^ 0 = 1_ K by GROUP_1:def 7;

then A2: S

A3: for n being Nat st S

S

proof

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

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

a |^ (n + 1) = (a |^ n) * a by Lm2;

hence a |^ (n + 1) <> 0. K by A4, A1, VECTSP_1:12; :: thesis: verum

end;assume A4: S

a |^ (n + 1) = (a |^ n) * a by Lm2;

hence a |^ (n + 1) <> 0. K by A4, A1, VECTSP_1:12; :: thesis: verum

hence a |^ n <> 0. K ; :: thesis: verum