let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds
+infty in rng v
let v be Valuation of K; :: thesis: ( K is having_valuation implies +infty in rng v )
assume K is having_valuation ; :: thesis: +infty in rng v
then A1: v . (0. K) = +infty by Def8;
dom v = the carrier of K by FUNCT_2:def 1;
hence +infty in rng v by A1, FUNCT_1:def 3; :: thesis: verum