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 & a <> 0. K holds
v . (a ") = - (v . a)
let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . (a ") = - (v . a)
let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . (a ") = - (v . a) )
assume that
A1: K is having_valuation and
A2: a <> 0. K ; :: thesis: v . (a ") = - (v . a)
a * (a ") = 1. K by A2, VECTSP_2:def 2;
then A3: (v . a) + (v . (a ")) = v . (1. K) by A1, Def8
.= 0 by A1, Th17 ;

now :: thesis: not a " = 0. K

assume a " = 0. K ; :: thesis: contradiction
then 1. K = a * (0. K) by A2, VECTSP_2:def 2
.= 0. K ;
hence contradiction ; :: thesis: verum

end;

then ( v . a in INT & v . (a ") in INT ) by A1, A2, Def8;
then reconsider w1 = v . a, w2 = v . (a ") as Element of REAL by XREAL_0:def 1;
w1 + w2 = 0 by A3, XXREAL_3:def 2;
then - w1 = w2 ;
hence v . (a ") = - (v . a) by XXREAL_3:def 3; :: thesis: verum