theorem Th27: :: GAUSSINT:27

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