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 multF of () = the multF of K | [:(),():] by ;
thus x1 * y1 = the multF of () . [x1,y1]
.= x * y by ; :: thesis: verum