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 3;
( card A = n & card A = m ) by A4, A5, A6;
hence n = m ; :: thesis: verum