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) . ((q0. I),u) = qadd ((q0. I),u) by Def12
.= u by Th12 ;
(quotadd I) . (u,(q0. I)) = qadd (u,(q0. I)) by Def12
.= u by Th12 ;
hence ( (quotadd I) . (u,(q0. I)) = u & (quotadd I) . ((q0. I),u) = u ) by A1; :: thesis: verum