theorem Th29: :: GAUSSINT:29

for z, w being G_RAT holds g_rat_mult . (z,w) = z * w