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