let R be commutative Ring; :: thesis: for r1, r2 being Element of R
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of (S ~ R) st x = Class ((EqRel S),((frac1 S) . r1)) & y = Class ((EqRel S),((frac1 S) . r2)) holds
x + y = Class ((EqRel S),((frac1 S) . (r1 + r2)))
let r1, r2 be Element of R; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x, y being Element of (S ~ R) st x = Class ((EqRel S),((frac1 S) . r1)) & y = Class ((EqRel S),((frac1 S) . r2)) holds
x + y = Class ((EqRel S),((frac1 S) . (r1 + r2)))
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y being Element of (S ~ R) st x = Class ((EqRel S),((frac1 S) . r1)) & y = Class ((EqRel S),((frac1 S) . r2)) holds
x + y = Class ((EqRel S),((frac1 S) . (r1 + r2)))
let x, y be Element of (S ~ R); :: thesis: ( x = Class ((EqRel S),((frac1 S) . r1)) & y = Class ((EqRel S),((frac1 S) . r2)) implies x + y = Class ((EqRel S),((frac1 S) . (r1 + r2))) )
reconsider rr1 = (frac1 S) . r1, rr2 = (frac1 S) . r2 as Element of Frac S ;
assume ( x = Class ((EqRel S),((frac1 S) . r1)) & y = Class ((EqRel S),((frac1 S) . r2)) ) ; :: thesis: x + y = Class ((EqRel S),((frac1 S) . (r1 + r2)))
then x + y = Class ((EqRel S),(rr1 + rr2)) by Th35;
hence x + y = Class ((EqRel S),((frac1 S) . (r1 + r2))) by Th26, Lm36; :: thesis: verum