theorem Th4: :: GAUSSINT:4

for z, w being G_INTEG holds g_int_add . (z,w) = z + w