let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of Quot. I st u <> q0. I holds
( (quotmult I) . u,((quotmultinv I) . u) = q1. I & (quotmult I) . ((quotmultinv I) . u),u = q1. I )
let u be Element of Quot. I; :: thesis: ( u <> q0. I implies ( (quotmult I) . u,((quotmultinv I) . u) = q1. I & (quotmult I) . ((quotmultinv I) . u),u = q1. I ) )
assume A1: u <> q0. I ; :: thesis: ( (quotmult I) . u,((quotmultinv I) . u) = q1. I & (quotmult I) . ((quotmultinv I) . u),u = q1. I )
A2: (quotmult I) . ((quotmultinv I) . u),u = (quotmult I) . (qmultinv u),u by Def15
.= qmult (qmultinv u),u by Def13
.= q1. I by A1, Th20 ;
(quotmult I) . u,((quotmultinv I) . u) = (quotmult I) . u,(qmultinv u) by Def15
.= qmult u,(qmultinv u) by Def13
.= q1. I by A1, Th20 ;
hence ( (quotmult I) . u,((quotmultinv I) . u) = q1. I & (quotmult I) . ((quotmultinv I) . u),u = q1. I ) by A2; :: thesis: verum