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;

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

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

let i be positive ExtInt; :: thesis: ( i in rng v implies 1. <= b_{1} )

assume i in rng v ; :: thesis: 1. <= b_{1}

end;assume i in rng v ; :: thesis: 1. <= b

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

end;

suppose
i is positive Real
; :: thesis: 1. <= b_{1}

then reconsider i1 = i as positive Real ;

ex p, q being Real st

( p = 1. & q = i & p <= q )

end;ex p, q being Real st

( p = 1. & q = i & p <= q )

proof

hence
1. <= i
; :: thesis: verum
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;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