let X be finite-dimensional RealLinearSpace; :: thesis: for b being OrdBasis of RLSp2RVSp X
for y being Element of (RLSp2RVSp X) holds y |-- b is Element of REAL (dim X)
let b be OrdBasis of RLSp2RVSp X; :: thesis: for y being Element of (RLSp2RVSp X) holds y |-- b is Element of REAL (dim X)
let y be Element of (RLSp2RVSp X); :: thesis: y |-- b is Element of REAL (dim X)
set z = y |-- b;
len (y |-- b) = len b by MATRLIN:def 7
.= dim (RLSp2RVSp X) by MATRLIN2:21
.= dim X by REAL_NS2:81 ;
hence y |-- b is Element of REAL (dim X) by FINSEQ_2:92; :: thesis: verum