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 & 0 <= v . ((1. K) + a) holds
0 <= v . a
let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) + a) holds
0 <= v . a
let v be Valuation of K; :: thesis: ( K is having_valuation & 0 <= v . ((1. K) + a) implies 0 <= v . a )
assume that
A1: ( K is having_valuation & 0 <= v . ((1. K) + a) ) and
A2: v . a < 0 ; :: thesis: contradiction
0 = v . (1. K) by A1, Th17;
hence contradiction by A1, A2, Th28; :: thesis: verum