theorem Th6: :: GAUSSINT:6

for z, w being G_INTEG holds g_int_mult . (z,w) = z * w