theorem :: GAUSSINT:33

for x being G_RAT holds Norm (x *') = Norm x ;