let n be Nat; :: thesis: for B being Subset of (RealVectSpace (Seg n)) st B = RN_Base n holds
B is Basis of RealVectSpace (Seg n)
let B be Subset of (RealVectSpace (Seg n)); :: thesis: ( B = RN_Base n implies B is Basis of RealVectSpace (Seg n) )
set V = RealVectSpace (Seg n);
assume A1: B = RN_Base n ; :: thesis: B is Basis of RealVectSpace (Seg n)
then reconsider B1 = B as R-orthonormal Subset of (RealVectSpace (Seg n)) ;
A2: the carrier of (Lin B) = { (Sum l) where l is Linear_Combination of B : verum } by RLVECT_3:def 2;

A3: now :: thesis: the carrier of (RealVectSpace (Seg n)) c= the carrier of (Lin B)

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

end;

the carrier of (Lin B) c= the carrier of (RealVectSpace (Seg 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 (RealVectSpace (Seg n)) )
assume x in the carrier of (Lin B) ; :: thesis: x in the carrier of (RealVectSpace (Seg n))
then ex l being Linear_Combination of B st x = Sum l by A2;
hence x in the carrier of (RealVectSpace (Seg n)) ; :: thesis: verum

end;

then the carrier of (Lin B) = the carrier of (RealVectSpace (Seg n)) by A3, XBOOLE_0:def 10;
then Lin B = RealVectSpace (Seg n) by Th8;
then B1 is Basis of RealVectSpace (Seg n) by RLVECT_3:def 3;
hence B is Basis of RealVectSpace (Seg n) ; :: thesis: verum