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

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