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