theorem Th29: :: QUOFIELD:29

for I being non degenerated commutative domRing-like Ring
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 )