theorem Th40: :: FVALUAT1:40

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 holds
( v . a is positive iff (normal-valuation v) . a is positive )