let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed 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 Th13;
then (v . (- (1. K))) + (v . (- (1. K))) = v . (1. K) by A1, Def10
.= 0 by A1, Th18 ;
hence v . (- (1. K)) = 0 by Th2; :: thesis: verum