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. <= b1 )
assume i in rng v ; :: thesis: 1. <= b1
per cases by XXREAL_3:1;
suppose i is positive Real ; :: thesis: 1. <= b1
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;
end;
end;
hence least-positive (rng v) = 1 by A1, A2, Def2; :: thesis: verum