let R be commutative Ring; for r1, r2 being Element of R
for S being non empty multiplicatively-closed Subset of R holds Fracmult (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 * r2) Fr_Eq S
let r1, r2 be Element of R; for S being non empty multiplicatively-closed Subset of R holds Fracmult (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 * r2) Fr_Eq S
let S be non empty multiplicatively-closed Subset of R; Fracmult (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 * r2) Fr_Eq S
A1:
(frac1 S) . r1 = [r1,(1. R)]
by Def4;
(frac1 S) . r2 = [r2,(1. R)]
by Def4;
then
Fracmult (((frac1 S) . r1),((frac1 S) . r2)) = (frac1 S) . (r1 * r2)
by A1, Def4;
hence
Fracmult (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 * r2) Fr_Eq S
by Th22; verum