let K be Field; :: thesis: for V being finite-dimensional VectSp of K
for b being OrdBasis of V
for W being Element of V holds dom (W |-- b) = dom b
let V be finite-dimensional VectSp of K; :: thesis: for b being OrdBasis of V
for W being Element of V holds dom (W |-- b) = dom b
let b be OrdBasis of V; :: thesis: for W being Element of V holds dom (W |-- b) = dom b
let W be Element of V; :: thesis: dom (W |-- b) = dom b
len (W |-- b) = len b by Def7;
hence dom (W |-- b) = dom b by FINSEQ_3:29; :: thesis: verum