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 & v . a < v . b holds

v . a = v . (a + b)

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

v . a = v . (a + b)

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

assume A1: ( K is having_valuation & v . a < v . b ) ; :: thesis: v . a = v . (a + b)

A2: min ((v . a),(v . b)) = v . a by A1, XXREAL_0:def 9;

A3: v . a <= v . (a + b) by A2, A1, Th27;

A4: a = a + (0. K) by RLVECT_1:def 4;

A5: 0. K = b - b by RLVECT_1:15;

A6: a = (a + b) - b by A4, A5, RLVECT_1:28

.= (a + b) + (- b) ;

A7: v . (- b) = v . b by A1, Th20;

A8: min ((v . (a + b)),(v . b)) <= v . a by A6, A7, A1, Th27;

then min ((v . (a + b)),(v . b)) = v . (a + b) by A1, XXREAL_0:def 9;

hence v . a = v . (a + b) by A3, A8, XXREAL_0:1; :: thesis: verum

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

v . a = v . (a + b)

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

v . a = v . (a + b)

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

assume A1: ( K is having_valuation & v . a < v . b ) ; :: thesis: v . a = v . (a + b)

A2: min ((v . a),(v . b)) = v . a by A1, XXREAL_0:def 9;

A3: v . a <= v . (a + b) by A2, A1, Th27;

A4: a = a + (0. K) by RLVECT_1:def 4;

A5: 0. K = b - b by RLVECT_1:15;

A6: a = (a + b) - b by A4, A5, RLVECT_1:28

.= (a + b) + (- b) ;

A7: v . (- b) = v . b by A1, Th20;

A8: min ((v . (a + b)),(v . b)) <= v . a by A6, A7, A1, Th27;

then min ((v . (a + b)),(v . b)) = v . (a + b) by A1, XXREAL_0:def 9;

hence v . a = v . (a + b) by A3, A8, XXREAL_0:1; :: thesis: verum