for V being RealUnitarySpace
for I being Basis of V
for v being VECTOR of V holds v in Lin I