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

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