V.L8 — Idempotence of Norm_omega

Norm_omega o Norm_omega = Norm_omega. At each stage n, NF_n maps into canonical representatives NFRep_n; applying NF_n to an element already in NFRep_n returns the same element.