let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S st x,y Fr_Eq S holds
y,x Fr_Eq S
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y being Element of Frac S st x,y Fr_Eq S holds
y,x Fr_Eq S
let x, y be Element of Frac S; :: thesis: ( x,y Fr_Eq S implies y,x Fr_Eq S )
assume x,y Fr_Eq S ; :: thesis: y,x Fr_Eq S
then consider s1 being Element of R such that
A2: s1 in S and
A3: (((x `1) * (y `2)) - ((y `1) * (x `2))) * s1 = 0. R ;
reconsider w = (y `1) * (x `2), v = (x `1) * (y `2) as Element of R ;
(w - v) * s1 = (- (v - w)) * s1 by VECTSP_1:17
.= - (0. R) by A3, VECTSP_1:9
.= 0. R ;
hence y,x Fr_Eq S by A2; :: thesis: verum