let i be Integer; :: 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 |^ i <> 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 |^ i <> 0. K
let a be Element of K; :: thesis: ( a <> 0. K implies a |^ i <> 0. K )
assume A1: a <> 0. K ; :: thesis: a |^ i <> 0. K

per cases ( 0 <= i or i < 0 ) ;

suppose 0 <= i ; :: thesis: a |^ i <> 0. K

then reconsider n1 = i as Element of NAT by INT_1:3;
a |^ i = a |^ n1 ;
hence a |^ i <> 0. K by A1, Lm3; :: thesis: verum

end;

suppose A2: i < 0 ; :: thesis: a |^ i <> 0. K

then reconsider n1 = - i as Element of NAT by INT_1:3;
A3: a |^ i = ((power K) . (a,|.i.|)) " by A2, Def5
.= (a |^ n1) " by A2, ABSVALUE:def 1 ;
a |^ n1 <> 0. K by A1, Lm3;
hence a |^ i <> 0. K by A3, VECTSP_2:13; :: thesis: verum

end;

end;