let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds

for x being Element of K

for y being Element of (ValuatRing v) st x = y holds

- x = - y

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of K

for y being Element of (ValuatRing v) st x = y holds

- x = - y )

set R = ValuatRing v;

set c = NonNegElements v;

assume A1: K is having_valuation ; :: thesis: for x being Element of K

for y being Element of (ValuatRing v) st x = y holds

- x = - y

let x be Element of K; :: thesis: for y being Element of (ValuatRing v) st x = y holds

- x = - y

let y be Element of (ValuatRing v); :: thesis: ( x = y implies - x = - y )

assume A2: x = y ; :: thesis: - x = - y

A3: 0 <= v . y by A1, A2, Th52;

v . (- x) = v . x by A1, Th20;

then reconsider x1 = - x as Element of (ValuatRing v) by A1, A2, A3, Th52;

x + (- x) = 0. K by RLVECT_1:def 10;

then y + x1 = 0. K by A2, A1, Th54

.= 0. (ValuatRing v) by A1, Def12 ;

hence - x = - y by RLVECT_1:def 10; :: thesis: verum

for x being Element of K

for y being Element of (ValuatRing v) st x = y holds

- x = - y

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of K

for y being Element of (ValuatRing v) st x = y holds

- x = - y )

set R = ValuatRing v;

set c = NonNegElements v;

assume A1: K is having_valuation ; :: thesis: for x being Element of K

for y being Element of (ValuatRing v) st x = y holds

- x = - y

let x be Element of K; :: thesis: for y being Element of (ValuatRing v) st x = y holds

- x = - y

let y be Element of (ValuatRing v); :: thesis: ( x = y implies - x = - y )

assume A2: x = y ; :: thesis: - x = - y

A3: 0 <= v . y by A1, A2, Th52;

v . (- x) = v . x by A1, Th20;

then reconsider x1 = - x as Element of (ValuatRing v) by A1, A2, A3, Th52;

x + (- x) = 0. K by RLVECT_1:def 10;

then y + x1 = 0. K by A2, A1, Th54

.= 0. (ValuatRing v) by A1, Def12 ;

hence - x = - y by RLVECT_1:def 10; :: thesis: verum