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