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 . a holds

(normal-valuation v) . a <= v . a

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & 0 <= v . a holds

(normal-valuation v) . a <= v . a

let v be Valuation of K; :: thesis: ( K is having_valuation & 0 <= v . a implies (normal-valuation v) . a <= v . a )

set f = normal-valuation v;

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: ( not 0 <= v . a or (normal-valuation v) . a <= v . a )

then A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;

assume 0 <= v . a ; :: thesis: (normal-valuation v) . a <= v . a

then A3: 0 <= (normal-valuation v) . a by A1, Th41;

0. + 1 <= least-positive (rng v) by Th10;

then ((normal-valuation v) . a) * 1 <= ((normal-valuation v) . a) * (least-positive (rng v)) by A3, Th3;

hence (normal-valuation v) . a <= v . a by A2, XXREAL_3:81; :: thesis: verum

for v being Valuation of K st K is having_valuation & 0 <= v . a holds

(normal-valuation v) . a <= v . a

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & 0 <= v . a holds

(normal-valuation v) . a <= v . a

let v be Valuation of K; :: thesis: ( K is having_valuation & 0 <= v . a implies (normal-valuation v) . a <= v . a )

set f = normal-valuation v;

set l = least-positive (rng v);

assume A1: K is having_valuation ; :: thesis: ( not 0 <= v . a or (normal-valuation v) . a <= v . a )

then A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;

assume 0 <= v . a ; :: thesis: (normal-valuation v) . a <= v . a

then A3: 0 <= (normal-valuation v) . a by A1, Th41;

0. + 1 <= least-positive (rng v) by Th10;

then ((normal-valuation v) . a) * 1 <= ((normal-valuation v) . a) * (least-positive (rng v)) by A3, Th3;

hence (normal-valuation v) . a <= v . a by A2, XXREAL_3:81; :: thesis: verum