let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x being Element of Frac S
for s being Element of S st x = [s,s] holds
x, 1. (R,S) Fr_Eq S
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x being Element of Frac S
for s being Element of S st x = [s,s] holds
x, 1. (R,S) Fr_Eq S
let x be Element of Frac S; :: thesis: for s being Element of S st x = [s,s] holds
x, 1. (R,S) Fr_Eq S
let s be Element of S; :: thesis: ( x = [s,s] implies x, 1. (R,S) Fr_Eq S )
assume A1: x = [s,s] ; :: thesis: x, 1. (R,S) Fr_Eq S
reconsider s1 = 1. R as Element of R ;
A2: (((x `1) * ((1. (R,S)) `2)) - (((1. (R,S)) `1) * (x `2))) * s1 = 0. R by A1, RLVECT_1:5;
s1 in S by C0SP1:def 4;
hence x, 1. (R,S) Fr_Eq S by A2; :: thesis: verum