let n be Nat; :: thesis: for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed 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 associative distributive Abelian add-associative right_zeroed 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₁[ Nat] means a |^ $1 <> 0. K;
a |^ 0 = 1_ K by GROUP_1:def 7;
then A2: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
a |^ (n + 1) = (a |^ n) * a by Lm4;
hence a |^ (n + 1) <> 0. K by A4, A1, VECTSP_1:12; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence a |^ n <> 0. K ; :: thesis: verum