let R be commutative Ring; :: thesis: 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)
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y, z being Element of Frac S holds Fracmult (x,(Fracmult (y,z))) = Fracmult ((Fracmult (x,y)),z)
let x, y, z be Element of Frac S; :: thesis: Fracmult (x,(Fracmult (y,z))) = Fracmult ((Fracmult (x,y)),z)
[((x `1) * ((y `1) * (z `1))),((x `2) * ((y `2) * (z `2)))] = [((x `1) * ((y `1) * (z `1))),(((x `2) * (y `2)) * (z `2))] by GROUP_1:def 3
.= Fracmult ((Fracmult (x,y)),z) by GROUP_1:def 3 ;
hence Fracmult (x,(Fracmult (y,z))) = Fracmult ((Fracmult (x,y)),z) ; :: thesis: verum