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