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 Th14 ;
(quotmult I) . (u,(q1. I)) = qmult (u,(q1. I)) by Def13
.= u by Th14 ;
hence ( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u ) by A1; :: thesis: verum