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 (ValuatRing v) 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 (ValuatRing v) 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 (ValuatRing v) st x = x1 & y = y1 holds

x + y = x1 + y1

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

x + y = x1 + y1

let x1, y1 be Element of (ValuatRing v); :: 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 (ValuatRing v) by A1, Def12;

A4: the addF of (ValuatRing v) = the addF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12;

thus x1 + y1 = the addF of (ValuatRing v) . [x1,y1]

.= x + y by A3, A4, A2, FUNCT_1:49 ; :: thesis: verum

for x, y being Element of K

for x1, y1 being Element of (ValuatRing v) 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 (ValuatRing v) 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 (ValuatRing v) st x = x1 & y = y1 holds

x + y = x1 + y1

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

x + y = x1 + y1

let x1, y1 be Element of (ValuatRing v); :: 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 (ValuatRing v) by A1, Def12;

A4: the addF of (ValuatRing v) = the addF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12;

thus x1 + y1 = the addF of (ValuatRing v) . [x1,y1]

.= x + y by A3, A4, A2, FUNCT_1:49 ; :: thesis: verum