theorem Lm65A: :: DUALSP02:5

for V being RealNormSpace st not V is trivial holds
ex F being Point of (DualSp V) st ||.F.|| = 1