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
A4: for I being Basis of V holds card I = n and
A5: for I being Basis of V holds card I = m ; :: thesis: n = m
consider A being finite Subset of V such that
A6: A is Basis of V by A1, MATRLIN:def 1;
card A = n by A4, A6;
hence n = m by A5, A6; :: thesis: verum