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