consider A being finite Subset of V such that
A2: A is Basis of V by A1, Def1;
consider n being Element of NAT such that
A3: n = card A ;
for I being Basis of V holds card I = n by A1, A2, A3, Th26;
hence ex b₁ being Element of NAT st
for I being Basis of V holds b₁ = card I ; :: thesis: verum