let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for o being object st o in the carrier of R holds
Class ((EqRel S),((frac1 S) . o)) in the carrier of (S ~ R)
let S be non empty multiplicatively-closed Subset of R; :: thesis: for o being object st o in the carrier of R holds
Class ((EqRel S),((frac1 S) . o)) in the carrier of (S ~ R)
let o be object ; :: thesis: ( o in the carrier of R implies Class ((EqRel S),((frac1 S) . o)) in the carrier of (S ~ R) )
assume o in the carrier of R ; :: thesis: Class ((EqRel S),((frac1 S) . o)) in the carrier of (S ~ R)
then reconsider a = (frac1 S) . o as Element of Frac S by FUNCT_2:5;
Class ((EqRel S),a) is Element of (S ~ R) by Lm41;
hence Class ((EqRel S),((frac1 S) . o)) in the carrier of (S ~ R) ; :: thesis: verum