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

( not v . a is negative iff not (normal-valuation v) . a is negative )

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

( not v . a is negative iff not (normal-valuation v) . a is negative )

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

set f = normal-valuation v;

set l = least-positive (rng v);

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

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

for v being Valuation of K st K is having_valuation holds

( not v . a is negative iff not (normal-valuation v) . a is negative )

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

( not v . a is negative iff not (normal-valuation v) . a is negative )

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

set f = normal-valuation v;

set l = least-positive (rng v);

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

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

per cases
( v . a is zero or (normal-valuation v) . a is zero or ( not v . a is zero & not (normal-valuation v) . a is zero ) )
;

end;

suppose
( v . a is zero or (normal-valuation v) . a is zero )
; :: thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )

end;

end;

suppose that A3:
not v . a is zero
and

A4: not (normal-valuation v) . a is zero ; :: thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )

A4: not (normal-valuation v) . a is zero ; :: thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )

thus
( not v . a is negative implies not (normal-valuation v) . a is negative )
by A1, A3, Th40; :: thesis: ( not (normal-valuation v) . a is negative implies not v . a is negative )

thus ( not (normal-valuation v) . a is negative implies not v . a is negative ) by A4, A1, Th40; :: thesis: verum

end;thus ( not (normal-valuation v) . a is negative implies not v . a is negative ) by A4, A1, Th40; :: thesis: verum