let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds len b1 = dim V1
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1 holds len b1 = dim V1
let b1 be OrdBasis of V1; :: thesis: len b1 = dim V1
reconsider R = rng b1 as Basis of V1 by MATRLIN:def 2;
A1: b1 is one-to-one by MATRLIN:def 2;
thus len b1 = card (Seg (len b1)) by FINSEQ_1:57
.= card (dom b1) by FINSEQ_1:def 3
.= card R by A1, CARD_1:70
.= dim V1 by VECTSP_9:def 1 ; :: thesis: verum