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

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