let R be commutative Ring; 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; 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; 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); ( 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) )
; 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; verum