let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of Quot. I holds
( (quotadd I) . u,(q0. I) = u & (quotadd I) . (q0. I),u = u )
let u be Element of Quot. I; :: thesis: ( (quotadd I) . u,(q0. I) = u & (quotadd I) . (q0. I),u = u )
A1: (quotadd I) . u,(q0. I) = qadd u,(q0. I) by Def12
.= u by Th14 ;
(quotadd I) . (q0. I),u = qadd (q0. I),u by Def12
.= u by Th14 ;
hence ( (quotadd I) . u,(q0. I) = u & (quotadd I) . (q0. I),u = u ) by A1; :: thesis: verum