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 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 :: thesis: for i being positive ExtInt st i in rng v holds
1. <= i

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 positive Real or i = +infty ) by XXREAL_3:1;

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

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

proof

reconsider jj = 1, i1 = i1 as Real ;
take jj ; :: thesis: ex q being Real st
( jj = 1. & q = i & jj <= q )
take i1 ; :: thesis: ( jj = 1. & i1 = i & jj <= i1 )
0 + 1 <= i1 by INT_1:7;
hence ( jj = 1. & i1 = i & jj <= 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, Def2; :: thesis: verum