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)) )
assume that
A1: x = Class ((EqRel S),a) and
A2: y = Class ((EqRel S),b) ; :: thesis: x * y = Class ((EqRel S),(a * b))
consider a1, b1 being Element of Frac S such that
A3: x = Class ((EqRel S),a1) and
A4: y = Class ((EqRel S),b1) and
A5: the multF of (S ~ R) . (x,y) = Class ((EqRel S),(a1 * b1)) by Def6;
A6: a1,a Fr_Eq S by A1, A3, Th26;
b1,b Fr_Eq S by A2, A4, Th26;
hence x * y = Class ((EqRel S),(a * b)) by A5, Th26, A6, Th27; :: thesis: verum