let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis:
let a be Element of K; :: thesis:
let v be Valuation of K; :: thesis:
assume A1: v . a = 1 ; :: thesis:
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:

let i be positive ExtInt; :: thesis:
assume i in rng v ; :: thesis:

per cases by XXREAL_3:1;

suppose i is positive Real ; :: thesis:

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:
take i1 ; :: thesis:
0 + 1 <= i1 by INT_1:7;
hence ( jj = 1. & i1 = i & jj <= i1 ) ; :: thesis:

end;

hence 1. <= i ; :: thesis:

end;

suppose i = +infty ; :: thesis:

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

end;

end;

end;

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