let n be Nat; :: thesis: for B being Subset of (REAL-L n) st B is Basis of REAL-L n holds
card B = n
let B be Subset of (REAL-L n); :: thesis: ( B is Basis of REAL-L n implies card B = n )
assume A1: B is Basis of REAL-L n ; :: thesis: card B = n
reconsider Br = RN_Base n as Subset of (REAL-L n) ;
Br is Basis of REAL-L n by Th54;
then card Br = card B by A1, RLVECT_5:26;
hence card B = n by Lm3; :: thesis: verum