let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of (the_Field_of_Quotients I) holds (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I)
let u, v be Element of (the_Field_of_Quotients I); :: thesis: (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I)
reconsider s = u, t = v as Element of Quot. I ;
(quotadd I) . (u,v) = qadd (s,t) by Def12;
hence (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I) ; :: thesis: verum