:: deftheorem defines Norm GAUSSINT:def 19 :
for z being G_RAT holds Norm z = z * (z *');