let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; :: thesis: for a being Element of K
for v being Valuation of K st v . a = 1 holds
least-positive (rng v) = 1
let a be Element of K; :: thesis: for v being Valuation of K st v . a = 1 holds
least-positive (rng v) = 1
let v be Valuation of K; :: thesis: ( v . a = 1 implies least-positive (rng v) = 1 )
assume A1: v . a = 1 ; :: thesis: least-positive (rng v) = 1
dom v = the carrier of K by FUNCT_2:def 1;
then A2: v . a in rng v by FUNCT_1:def 3;

now

let i be positive ExtInt; :: thesis: ( i in rng v implies 1. <= b₁ )
assume i in rng v ; :: thesis: 1. <= b₁

per cases ( i is real positive number or i = +infty ) by XXREAL_3:1;

suppose i is real positive number ; :: thesis: 1. <= b₁

then reconsider i1 = i as real positive number ;
ex p, q being Real st
( p = 1. & q = i & p <= q )

proof

reconsider i1 = i1 as Real by XREAL_0:def 1;
take 1 ; :: thesis: ex q being Real st
( 1 = 1. & q = i & 1 <= q )
take i1 ; :: thesis: ( 1 = 1. & i1 = i & 1 <= i1 )
0 + 1 <= i1 by INT_1:7;
hence ( 1 = 1. & i1 = i & 1 <= i1 ) ; :: thesis: verum

end;

hence 1. <= i ; :: thesis: verum

end;

suppose i = +infty ; :: thesis: 1. <= b₁

hence 1. <= i by XXREAL_0:3; :: thesis: verum

end;

end;

end;

hence least-positive (rng v) = 1 by A1, A2, Def4; :: thesis: verum