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

+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