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
v . (- (1. K)) = 0
let v be Valuation of K; :: thesis: ( K is having_valuation implies v . (- (1. K)) = 0 )
assume A1: K is having_valuation ; :: thesis: v . (- (1. K)) = 0
(- (1. K)) * (- (1. K)) = 1. K by Th12;
then (v . (- (1. K))) + (v . (- (1. K))) = v . (1. K) by A1, Def8
.= 0 by A1, Th17 ;
hence v . (- (1. K)) = 0 by Th2; :: thesis: verum