theorem Th29: :: FVALUAT1:29

for i being Integer
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
for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . (a |^ i) = i * (v . a)