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