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 in S holds
Class ((EqRel S),a) is Unit of (S ~ R)
let S be non empty multiplicatively-closed Subset of R; :: thesis: for a being Element of Frac S st a `1 in S holds
Class ((EqRel S),a) is Unit of (S ~ R)
let a be Element of Frac S; :: thesis: ( a `1 in S implies Class ((EqRel S),a) is Unit of (S ~ R) )
assume a `1 in S ; :: thesis: Class ((EqRel S),a) is Unit of (S ~ R)
then reconsider b = [(a `2),(a `1)] as Element of Frac S by Def3;
A2: (a * b) `1 = (a * b) `2 ;
reconsider x = Class ((EqRel S),a), y = Class ((EqRel S),b) as Element of (S ~ R) by Lm41;
A3: x * y = Class ((EqRel S),(a * b)) by Th33
.= 1. (S ~ R) by A2, Lm42 ;
A4: x divides 1. (S ~ R) by A3;
x is unital by A4;
hence Class ((EqRel S),a) is Unit of (S ~ R) ; :: thesis: verum