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 K is having_valuation & a <> 0. K holds

v . a <> +infty

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . a <> +infty

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . a <> +infty )

assume ( K is having_valuation & a <> 0. K ) ; :: thesis: v . a <> +infty

then v . a in INT by Def8;

hence v . a <> +infty ; :: thesis: verum

for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . a <> +infty

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . a <> +infty

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . a <> +infty )

assume ( K is having_valuation & a <> 0. K ) ; :: thesis: v . a <> +infty

then v . a in INT by Def8;

hence v . a <> +infty ; :: thesis: verum