let n be Element of NAT ; :: thesis: RN_Base n is Basis of REAL-US n
reconsider B = RN_Base n as Subset of (REAL-US n) by REAL_NS1:def 6;
set V = REAL-US n;
A1: the carrier of (Lin B) = { (Sum l) where l is Linear_Combination of B : verum } by RUSUB_3:def 1;

A2: now :: thesis: the carrier of (REAL-US n) c= the carrier of (Lin B)

assume not the carrier of (REAL-US n) c= the carrier of (Lin B) ; :: thesis: contradiction
then consider x being object such that
A3: x in the carrier of (REAL-US n) and
A4: not x in the carrier of (Lin B) ;
reconsider x0 = x as Element of (REAL-US n) by A3;
ex l being Linear_Combination of B st x0 = Sum l by Th43;
hence contradiction by A1, A4; :: thesis: verum

end;

the carrier of (Lin B) c= the carrier of (REAL-US n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Lin B) or x in the carrier of (REAL-US n) )
assume x in the carrier of (Lin B) ; :: thesis: x in the carrier of (REAL-US n)
then ex l being Linear_Combination of B st x = Sum l by A1;
hence x in the carrier of (REAL-US n) ; :: thesis: verum

end;

then the carrier of (Lin B) = the carrier of (REAL-US n) by A2, XBOOLE_0:def 10;
then Lin B = REAL-US n by RUSUB_1:26;
hence RN_Base n is Basis of REAL-US n by RUSUB_3:def 2; :: thesis: verum