let n, m be Nat; :: thesis: ( ( for I being Basis of V holds n = card I ) & ( for I being Basis of V holds m = card I ) implies n = m )
assume that
A3: for I being Basis of V holds card I = n and
A4: for I being Basis of V holds card I = m ; :: thesis: n = m
consider A being finite Subset of V such that
A5: A is Basis of V by Def3;
card A = n by A3, A5;
hence n = m by A4, A5; :: thesis: verum