let R be commutative Ring; :: thesis: for r1, r2 being Element of R
for S being non empty multiplicatively-closed Subset of R holds Fracadd (((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 Fracadd (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 + r2) Fr_Eq S
let S be non empty multiplicatively-closed Subset of R; :: thesis: Fracadd (((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 Fracadd (((frac1 S) . r1),((frac1 S) . r2)) = (frac1 S) . (r1 + r2) by A1, Def4;
hence Fracadd (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 + r2) Fr_Eq S by Th22; :: thesis: verum