let x be G_INTEG; :: thesis: ( Norm x = 0 implies x = 0 )
A1: Norm x = ((Re x) + ((Im x) * <i>)) * ((Re x) - ((Im x) * <i>)) by COMPLEX1:13
.= ((Re x) ^2) + ((Im x) ^2) ;
assume Norm x = 0 ; :: thesis: x = 0
hence x = 0 by A1, COMPLEX1:5; :: thesis: verum