let V be free finite-rank Z_Module; :: 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