let n be Nat; :: thesis: dim (RealVectSpace (Seg n)) = n
reconsider B = RN_Base n as Subset of (RealVectSpace (Seg n)) by FINSEQ_2:93;
A1: for I being Basis of RealVectSpace (Seg n) holds n = card I

proof

let I be Basis of RealVectSpace (Seg n); :: thesis: n = card I
B is Basis of RealVectSpace (Seg n) by Th44;
then card B = card I by RLVECT_5:25;
hence n = card I by Lm5; :: thesis: verum

end;

n in NAT by ORDINAL1:def 12;
hence dim (RealVectSpace (Seg n)) = n by A1, RLVECT_5:def 2; :: thesis: verum