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