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

( 0 <= v . a iff 0 <= (normal-valuation v) . a )

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

( 0 <= v . a iff 0 <= (normal-valuation v) . a )

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

set f = normal-valuation v;

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

then ( (normal-valuation v) . a is positive or 0 = (normal-valuation v) . a ) ;

hence 0 <= v . a by A1, Th40, Th37; :: thesis: verum

for v being Valuation of K st K is having_valuation holds

( 0 <= v . a iff 0 <= (normal-valuation v) . a )

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

( 0 <= v . a iff 0 <= (normal-valuation v) . a )

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

set f = normal-valuation v;

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

hereby :: thesis: ( 0 <= (normal-valuation v) . a implies 0 <= v . a )

assume
0 <= (normal-valuation v) . a
; :: thesis: 0 <= v . aassume
0 <= v . a
; :: thesis: 0 <= (normal-valuation v) . a

then ( v . a is positive or 0 = v . a ) ;

hence 0 <= (normal-valuation v) . a by A1, Th40, Th37; :: thesis: verum

end;then ( v . a is positive or 0 = v . a ) ;

hence 0 <= (normal-valuation v) . a by A1, Th40, Th37; :: thesis: verum

then ( (normal-valuation v) . a is positive or 0 = (normal-valuation v) . a ) ;

hence 0 <= v . a by A1, Th40, Th37; :: thesis: verum