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
A2: v . (1. K) = v . ((1. K) * (1. K))
.= (v . (1. K)) + (v . (1. K)) by A1, Def8 ;
v . (1. K) in INT by A1, Def8;
then reconsider x = v . (1. K) as Element of REAL by XREAL_0:def 1;
x + 0 = x + x by A2, XXREAL_3:def 2;
hence v . (1. K) = 0 ; :: thesis: verum