theorem Th28: :: FVALUAT1:28

for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b being Element of K
for v being Valuation of K st K is having_valuation & v . a < v . b holds
v . a = v . (a + b)