theorem Th25: :: QUOFIELD:25

for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I holds
( (quotmult I) . (u,(q1. I)) = u & (quotmult I) . ((q1. I),u) = u )