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