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 )
hereby :: thesis: ( 0 <= (normal-valuation v) . a implies 0 <= v . a )
assume 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;
assume 0 <= (normal-valuation v) . a ; :: thesis: 0 <= 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