let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed 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 Def12;
reconsider l1 = least-positive (rng v) as Real by A1, Lm7;

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

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

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

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

then reconsider va = v . a as real positive number ;
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 number 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 Real by A4, A5, A2, XXREAL_3:73;
va = c * b by A1, Def12, A5;
hence (normal-valuation v) . a is positive by A5; :: thesis: verum

end;

suppose v . a = +infty ; :: thesis: (normal-valuation v) . a is positive

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

end;

end;

end;

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

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

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

then reconsider fa = (normal-valuation v) . a as real positive number ;
v . a = fa * l1 by A2, XXREAL_3:def 5;
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 A1, Th41; :: thesis: verum

end;

end;