theorem Th20: :: RINGFRAC:13

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S holds Fracmult (x,(Fracmult (y,z))) = Fracmult ((Fracmult (x,y)),z)