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