theorem Th16: :: DUALSP06:16

for V being RealNormSpace
for M being Subspace of V
for v being VECTOR of (DualSp V)
for m being VECTOR of V st v in Ort_Comp M & m in M holds
m .|. v = 0