theorem Th17: :: CLOPBAN2:17

for X being non trivial ComplexNormSpace ex w being VECTOR of X st ||.w.|| = 1