let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for a being Element of Frac S st a `1 = a `2 holds
Class ((EqRel S),a) = 1. (S ~ R)
let S be non empty multiplicatively-closed Subset of R; :: thesis: for a being Element of Frac S st a `1 = a `2 holds
Class ((EqRel S),a) = 1. (S ~ R)
let a be Element of Frac S; :: thesis: ( a `1 = a `2 implies Class ((EqRel S),a) = 1. (S ~ R) )
assume A1: a `1 = a `2 ; :: thesis: Class ((EqRel S),a) = 1. (S ~ R)
reconsider s1 = 1. R as Element of S by C0SP1:def 4;
(((a `1) * ((1. (R,S)) `2)) - (((1. (R,S)) `1) * (a `2))) * s1 = 0. R by A1, RLVECT_1:5;
then a, 1. (R,S) Fr_Eq S ;
then Class ((EqRel S),a) = Class ((EqRel S),(1. (R,S))) by Th26
.= 1. (S ~ R) by Def6 ;
hence Class ((EqRel S),a) = 1. (S ~ R) ; :: thesis: verum