for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for W1 being Subspace of V1 st W1 = (Omega). V1 holds
for w being Vector of W1
for v being Vector of V1
for w1 being OrdBasis of W1 st v = w & b1 = w1 holds
v |-- b1 = w |-- w1