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