for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I st u <> q0. I holds
( qmult (u,(qmultinv u)) = q1. I & qmult ((qmultinv u),u) = q1. I )