let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds
least-positive (rng v) is integer
let v be Valuation of K; :: thesis: ( K is having_valuation implies least-positive (rng v) is integer )
set l = least-positive (rng v);
assume A1: K is having_valuation ; :: thesis: least-positive (rng v) is integer
then consider a being Element of K such that
A2: v . a <> 0 and
A3: v . a <> +infty by Def10;
A4: dom v = the carrier of K by FUNCT_2:def 1;
then A5: v . a in rng v by FUNCT_1:def 3;
assume not least-positive (rng v) is integer ; :: thesis: contradiction
then A6: least-positive (rng v) = +infty by Def1;
A7: a <> 0. K by A1, A3, Def10;
then A8: v . a in INT by A1, Def10;
reconsider va = v . a as Real by A8;

per cases ( va is positive or not va is positive ) ;

suppose va is positive ; :: thesis: contradiction

then least-positive (rng v) <= v . a by A5, Def4;
hence contradiction by A3, A6, XXREAL_0:4; :: thesis: verum

end;

suppose not va is positive ; :: thesis: contradiction

then reconsider va = va as real non positive number ;
reconsider va = va as real negative number by A2;
set b = a " ;
a " <> 0. K by A7, VECTSP_2:13;
then A9: v . (a ") in INT by A1, Def10;
A10: v . (a ") in rng v by A4, FUNCT_1:def 3;
v . (a ") = - (v . a) by A1, A7, Th22
.= - va by XXREAL_3:def 3 ;
then least-positive (rng v) <= v . (a ") by A10, Def4;
hence contradiction by A9, A6, XXREAL_0:4; :: thesis: verum

end;

end;