theorem Th96: :: RING_3:97

for F being 0 -characteristic Field
for i, j being non zero Integer st j divides i holds
(i div j) '*' (1. F) = (i '*' (1. F)) * ((j '*' (1. F)) ")