consider A being finite Subset of V such that
A2: A is Basis of V by A1;
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, Th5;
hence ex b₁ being Element of NAT st
for I being Basis of V holds b₁ = card I ; :: thesis: verum