let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a, b being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K holds

v . (a / b) = - (v . (b / a))

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K holds

v . (a / b) = - (v . (b / a))

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K & b <> 0. K implies v . (a / b) = - (v . (b / a)) )

assume A1: K is having_valuation ; :: thesis: ( not a <> 0. K or not b <> 0. K or v . (a / b) = - (v . (b / a)) )

assume A2: a <> 0. K ; :: thesis: ( not b <> 0. K or v . (a / b) = - (v . (b / a)) )

assume b <> 0. K ; :: thesis: v . (a / b) = - (v . (b / a))

hence v . (a / b) = (v . a) - (v . b) by A1, Th22

.= - ((v . b) - (v . a)) by XXREAL_3:26

.= - (v . (b / a)) by A1, A2, Th22 ;

:: thesis: verum

for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K holds

v . (a / b) = - (v . (b / a))

let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K holds

v . (a / b) = - (v . (b / a))

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K & b <> 0. K implies v . (a / b) = - (v . (b / a)) )

assume A1: K is having_valuation ; :: thesis: ( not a <> 0. K or not b <> 0. K or v . (a / b) = - (v . (b / a)) )

assume A2: a <> 0. K ; :: thesis: ( not b <> 0. K or v . (a / b) = - (v . (b / a)) )

assume b <> 0. K ; :: thesis: v . (a / b) = - (v . (b / a))

hence v . (a / b) = (v . a) - (v . b) by A1, Th22

.= - ((v . b) - (v . a)) by XXREAL_3:26

.= - (v . (b / a)) by A1, A2, Th22 ;

:: thesis: verum