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 Th33;
hence x * y = Class ((EqRel S),((frac1 S) . (r1 * r2))) by Th26, Lm38; :: thesis: verum