for z, w being G_RAT holds g_rat_add . (z,w) = z + w