theorem Th27: :: QUOFIELD:27

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