theorem Th17: :: REAL_NS3:16

for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for y being Element of (RLSp2RVSp X) holds y |-- b is Element of REAL (dim X)