let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for a, b being Element of Frac S
for x, y being Element of (S ~ R) st x = Class ((EqRel S),a) & y = Class ((EqRel S),b) holds
x + y = Class ((EqRel S),(a + b))
let S be non empty multiplicatively-closed Subset of R; :: thesis: for a, b being Element of Frac S
for x, y being Element of (S ~ R) st x = Class ((EqRel S),a) & y = Class ((EqRel S),b) holds
x + y = Class ((EqRel S),(a + b))
let a, b be Element of Frac S; :: thesis: for x, y being Element of (S ~ R) st x = Class ((EqRel S),a) & y = Class ((EqRel S),b) holds
x + y = Class ((EqRel S),(a + b))
let x, y be Element of (S ~ R); :: thesis: ( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) implies x + y = Class ((EqRel S),(a + b)) )
consider a1, b1 being Element of Frac S such that
A1: ( x = Class ((EqRel S),a1) & y = Class ((EqRel S),b1) ) and
A2: the addF of (S ~ R) . (x,y) = Class ((EqRel S),(a1 + b1)) by Def6;
assume ( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) ) ; :: thesis: x + y = Class ((EqRel S),(a + b))
then ( a,a1 Fr_Eq S & b,b1 Fr_Eq S ) by A1, Th26;
hence x + y = Class ((EqRel S),(a + b)) by A2, Th26, Th28; :: thesis: verum