let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of Quot. I holds
( (quotmult I) . u,(q1. I) = u & (quotmult I) . (q1. I),u = u )
let u be Element of Quot. I; :: thesis: ( (quotmult I) . u,(q1. I) = u & (quotmult I) . (q1. I),u = u )
A1: (quotmult I) . (q1. I),u = qmult (q1. I),u by Def13
.= u by Th16 ;
(quotmult I) . u,(q1. I) = qmult u,(q1. I) by Def13
.= u by Th16 ;
hence ( (quotmult I) . u,(q1. I) = u & (quotmult I) . (q1. I),u = u ) by A1; :: thesis: verum