let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a, b being Element of K

for v being Valuation of K st K is having_valuation & b is Element of (ValuatRing v) holds

v . a <= (v . a) + (v . b)

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & b is Element of (ValuatRing v) holds

v . a <= (v . a) + (v . b)

let v be Valuation of K; :: thesis: ( K is having_valuation & b is Element of (ValuatRing v) implies v . a <= (v . a) + (v . b) )

assume A1: K is having_valuation ; :: thesis: ( not b is Element of (ValuatRing v) or v . a <= (v . a) + (v . b) )

assume b is Element of (ValuatRing v) ; :: thesis: v . a <= (v . a) + (v . b)

then 0 <= v . b by A1, Th52;

then (v . a) + 0 <= (v . a) + (v . b) by XXREAL_3:35;

hence v . a <= (v . a) + (v . b) by XXREAL_3:4; :: thesis: verum

for v being Valuation of K st K is having_valuation & b is Element of (ValuatRing v) holds

v . a <= (v . a) + (v . b)

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & b is Element of (ValuatRing v) holds

v . a <= (v . a) + (v . b)

let v be Valuation of K; :: thesis: ( K is having_valuation & b is Element of (ValuatRing v) implies v . a <= (v . a) + (v . b) )

assume A1: K is having_valuation ; :: thesis: ( not b is Element of (ValuatRing v) or v . a <= (v . a) + (v . b) )

assume b is Element of (ValuatRing v) ; :: thesis: v . a <= (v . a) + (v . b)

then 0 <= v . b by A1, Th52;

then (v . a) + 0 <= (v . a) + (v . b) by XXREAL_3:35;

hence v . a <= (v . a) + (v . b) by XXREAL_3:4; :: thesis: verum