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

for v being Valuation of K st K is having_valuation holds

v . (- a) = v . a

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

v . (- a) = v . a

let v be Valuation of K; :: thesis: ( K is having_valuation implies v . (- a) = v . a )

assume A1: K is having_valuation ; :: thesis: v . (- a) = v . a

(- (1. K)) * a = - a by VECTSP_2:29;

hence v . (- a) = (v . (- (1. K))) + (v . a) by A1, Def8

.= 0 + (v . a) by A1, Th19

.= v . a by XXREAL_3:4 ;

:: thesis: verum

for v being Valuation of K st K is having_valuation holds

v . (- a) = v . a

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

v . (- a) = v . a

let v be Valuation of K; :: thesis: ( K is having_valuation implies v . (- a) = v . a )

assume A1: K is having_valuation ; :: thesis: v . (- a) = v . a

(- (1. K)) * a = - a by VECTSP_2:29;

hence v . (- a) = (v . (- (1. K))) + (v . a) by A1, Def8

.= 0 + (v . a) by A1, Th19

.= v . a by XXREAL_3:4 ;

:: thesis: verum