consider A being finite Subset of V such that
A2: A is Basis of V by A1, MATRLIN:def 1;
consider n being Nat such that
A3: n = card A ;
for I being Basis of V holds card I = n by A1, A2, A3, Th22;
hence ex b₁ being Nat st
for I being Basis of V holds b₁ = card I ; :: thesis: verum