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
+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 Def10;
dom v = the carrier of K by FUNCT_2:def 1;
hence +infty in rng v by A1, FUNCT_1:def 3; :: thesis: verum