for x being G_INTEG st Norm x = 0 holds
x = 0