let n be Nat; :: thesis: dim (REAL-L n) = n
reconsider B = RN_Base n as Subset of (REAL-L n) ;
A: n in NAT by ORDINAL1:def 13;
for I being Basis of REAL-L n holds n = card I

proof

let I be Basis of REAL-L n; :: thesis: n = card I
B is Basis of REAL-L n by Th54;
then card B = card I by RLVECT_5:26;
hence n = card I by Lm3; :: thesis: verum

end;

hence dim (REAL-L n) = n by A, RLVECT_5:def 3; :: thesis: verum