|.(0. F_Complex).| = 0 by Def1, COMPLEX1:44;