let x, y be G_RAT; :: thesis: Norm (x * y) = (Norm x) * (Norm y)
thus Norm (x * y) = (x * y) * ((x *') * (y *')) by COMPLEX1:35
.= (Norm x) * (Norm y) ; :: thesis: verum