let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds
for x, y being Element of K
for x1, y1 being Element of () st x = x1 & y = y1 holds
x + y = x1 + y1

let v be Valuation of K; :: thesis: ( K is having_valuation implies for x, y being Element of K
for x1, y1 being Element of () st x = x1 & y = y1 holds
x + y = x1 + y1 )

set R = ValuatRing v;
set c = NonNegElements v;
assume A1: K is having_valuation ; :: thesis: for x, y being Element of K
for x1, y1 being Element of () st x = x1 & y = y1 holds
x + y = x1 + y1

let x, y be Element of K; :: thesis: for x1, y1 being Element of () st x = x1 & y = y1 holds
x + y = x1 + y1

let x1, y1 be Element of (); :: thesis: ( x = x1 & y = y1 implies x + y = x1 + y1 )
assume A2: ( x = x1 & y = y1 ) ; :: thesis: x + y = x1 + y1
A3: NonNegElements v = the carrier of () by ;
A4: the addF of () = the addF of K | [:(),():] by ;
thus x1 + y1 = the addF of () . [x1,y1]
.= x + y by ; :: thesis: verum