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 () . 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 () . a is positive )

let v be Valuation of K; :: thesis: ( K is having_valuation implies ( v . a is positive iff () . 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 () . a is positive )
then A2: v . a = (() . a) * () by Def10;
reconsider l1 = least-positive (rng v) as Element of REAL by ;
hereby :: thesis: ( () . a is positive implies v . a is positive )
assume A3: v . a is positive ; :: thesis: () . a is positive
per cases ( v . a is positive Real or v . a = +infty ) by ;
suppose v . a is positive Real ; :: thesis: () . 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 ;
then consider c, b being Complex such that
A5: ( (normal-valuation v) . a = c & l1 = b & (() . a) * l1 = c * b ) by XXREAL_3:def 5;
reconsider c = c as Element of REAL by ;
va = c * b by ;
hence (normal-valuation v) . a is positive by A5; :: thesis: verum
end;
end;
end;
assume A6: (normal-valuation v) . a is positive ; :: thesis: v . a is positive
per cases ) . a is positive Real or () . a = +infty ) by ;
suppose (normal-valuation v) . a is positive Real ; :: thesis: v . a is positive
then reconsider fa = () . a as positive Real ;
v . a = fa * l1 by ;
hence v . a is positive ; :: thesis: verum
end;
suppose (normal-valuation v) . a = +infty ; :: thesis: v . a is positive
hence v . a is positive by ; :: thesis: verum
end;
end;