let q be G_RAT; :: thesis: Norm q = (|.(Re q).| ^2) + (|.(Im q).| ^2)
A1: |.(Re q).| ^2 = (Re q) ^2 by COMPLEX1:75;
thus Norm q = ((Re q) + ((Im q) * <i>)) * ((Re q) - ((Im q) * <i>)) by COMPLEX1:13
.= ((Re q) ^2) + ((Im q) ^2)
.= (|.(Re q).| ^2) + (|.(Im q).| ^2) by A1, COMPLEX1:75 ; :: thesis: verum