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 is positive iff (normal-valuation v) . a is positive )

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

( v . a is positive iff (normal-valuation v) . a is positive )

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

set f = normal-valuation v;

set l = least-positive (rng v);

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

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

reconsider l1 = least-positive (rng v) as Element of REAL by A1, Lm6;

for v being Valuation of K st K is having_valuation holds

( v . a is positive iff (normal-valuation v) . a is positive )

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

( v . a is positive iff (normal-valuation v) . a is positive )

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

set f = normal-valuation v;

set l = least-positive (rng v);

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

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

reconsider l1 = least-positive (rng v) as Element of REAL by A1, Lm6;

hereby :: thesis: ( (normal-valuation v) . a is positive implies v . a is positive )

assume A6:
(normal-valuation v) . a is positive
; :: thesis: v . a is positive assume A3:
v . a is positive
; :: thesis: (normal-valuation v) . a is positive

end;per cases
( v . a is positive Real or v . a = +infty )
by A3, XXREAL_3:1;

end;

suppose
v . a is positive Real
; :: thesis: (normal-valuation v) . a is positive

then reconsider va = v . a as positive Real ;

A4: va in REAL by XREAL_0:def 1;

then (normal-valuation v) . a in REAL by A2, XXREAL_3:73;

then consider c, b being Complex such that

A5: ( (normal-valuation v) . a = c & l1 = b & ((normal-valuation v) . a) * l1 = c * b ) by XXREAL_3:def 5;

reconsider c = c as Element of REAL by A4, A5, A2, XXREAL_3:73;

va = c * b by A1, Def10, A5;

hence (normal-valuation v) . a is positive by A5; :: thesis: verum

end;A4: va in REAL by XREAL_0:def 1;

then (normal-valuation v) . a in REAL by A2, XXREAL_3:73;

then consider c, b being Complex such that

A5: ( (normal-valuation v) . a = c & l1 = b & ((normal-valuation v) . a) * l1 = c * b ) by XXREAL_3:def 5;

reconsider c = c as Element of REAL by A4, A5, A2, XXREAL_3:73;

va = c * b by A1, Def10, A5;

hence (normal-valuation v) . a is positive by A5; :: thesis: verum

per cases
( (normal-valuation v) . a is positive Real or (normal-valuation v) . a = +infty )
by A6, XXREAL_3:1;

end;

suppose
(normal-valuation v) . a is positive Real
; :: thesis: v . a is positive

then reconsider fa = (normal-valuation v) . a as positive Real ;

v . a = fa * l1 by A2, XXREAL_3:def 5;

hence v . a is positive ; :: thesis: verum

end;v . a = fa * l1 by A2, XXREAL_3:def 5;

hence v . a is positive ; :: thesis: verum