theorem :: CLVECT_1:102

for CNS being ComplexNormSpace holds ||.(0. CNS).|| = 0 ;