let R be commutative Ring; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum