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, Th18 ;
(quotmult I) . (u,((quotmultinv I) . u)) = (quotmult I) . (u,(qmultinv u)) by Def15
.= qmult (u,(qmultinv u)) by Def13
.= q1. I by A1, Th18 ;
hence ( (quotmult I) . (u,((quotmultinv I) . u)) = q1. I & (quotmult I) . (((quotmultinv I) . u),u) = q1. I ) by A2; :: thesis: verum