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 holds

( v . a = +infty iff (normal-valuation v) . a = +infty )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

( v . a = +infty iff (normal-valuation v) . a = +infty )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( v . a = +infty iff (normal-valuation v) . a = +infty ) )

assume A1: K is having_valuation ; :: thesis: ( v . a = +infty iff (normal-valuation v) . a = +infty )

set f = normal-valuation v;

set l = least-positive (rng v);

A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by A1, Def10;

least-positive (rng v) is integer by A1, Th35;

hence ( v . a = +infty implies (normal-valuation v) . a = +infty ) by A2, XXREAL_3:69; :: thesis: ( (normal-valuation v) . a = +infty implies v . a = +infty )

thus ( (normal-valuation v) . a = +infty implies v . a = +infty ) by A2, XXREAL_3:def 5; :: thesis: verum

for v being Valuation of K st K is having_valuation holds

( v . a = +infty iff (normal-valuation v) . a = +infty )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds

( v . a = +infty iff (normal-valuation v) . a = +infty )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( v . a = +infty iff (normal-valuation v) . a = +infty ) )

assume A1: K is having_valuation ; :: thesis: ( v . a = +infty iff (normal-valuation v) . a = +infty )

set f = normal-valuation v;

set l = least-positive (rng v);

A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by A1, Def10;

least-positive (rng v) is integer by A1, Th35;

hence ( v . a = +infty implies (normal-valuation v) . a = +infty ) by A2, XXREAL_3:69; :: thesis: ( (normal-valuation v) . a = +infty implies v . a = +infty )

thus ( (normal-valuation v) . a = +infty implies v . a = +infty ) by A2, XXREAL_3:def 5; :: thesis: verum