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

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