let n, m be Element of 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;

card A = n by A4, A6;

hence n = m by A5, A6; :: thesis: verum

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;

card A = n by A4, A6;

hence n = m by A5, A6; :: thesis: verum