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 and
A2: 0 <= v . ((1. K) - a) ; :: thesis: 0 <= v . a
( (1. K) - a = (1. K) + (- a) & v . (- a) = v . a ) by A1, Th20;
hence 0 <= v . a by A1, A2, Th30; :: thesis: verum