let n be Element of NAT ; :: thesis: dim (REAL-US n) = n
reconsider B = RN_Base n as Subset of (REAL-US n) by REAL_NS1:def 6;
for I being Basis of REAL-US n holds n = card I

proof

let I be Basis of REAL-US n; :: thesis: n = card I
B is Basis of REAL-US n by Th48;
then card B = card I by RUSUB_4:5;
hence n = card I by Lm5; :: thesis: verum

end;

hence dim (REAL-US n) = n by RUSUB_4:def 2; :: thesis: verum