theorem Th34: :: GAUSSINT:34

for x, y being G_RAT holds Norm (x * y) = (Norm x) * (Norm y)