theorem Th17: :: LOPBAN_2:17

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