theorem Th43: :: GAUSSINT:43

for x, y being G_INTEG st x is_associated_to y holds
x *' is_associated_to y *'