let n be Nat; :: thesis: for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
[#] (Lin Ar) = [#] (Lin At)
let Ar be Subset of (REAL-NS n); :: thesis: for At being Subset of (TOP-REAL n) st Ar = At holds
[#] (Lin Ar) = [#] (Lin At)
let At be Subset of (TOP-REAL n); :: thesis: ( Ar = At implies [#] (Lin Ar) = [#] (Lin At) )
assume A1: Ar = At ; :: thesis: [#] (Lin Ar) = [#] (Lin At)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [#] (Lin At) c= [#] (Lin Ar)

let x be object ; :: thesis: ( x in [#] (Lin Ar) implies x in [#] (Lin At) )
assume x in [#] (Lin Ar) ; :: thesis: x in [#] (Lin At)
then x in Lin Ar ;
then consider L being Linear_Combination of Ar such that
A2: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of TOP-REAL n by Th11;
( Carrier L1 = Carrier L & Carrier L c= Ar ) by RLVECT_2:def 6;
then A3: L1 is Linear_Combination of At by A1, RLVECT_2:def 6;
Sum L1 = Sum L by Th23;
then x in Lin At by A2, A3, RLVECT_3:14;
hence x in [#] (Lin At) ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (Lin At) or x in [#] (Lin Ar) )
assume x in [#] (Lin At) ; :: thesis: x in [#] (Lin Ar)
then x in Lin At ;
then consider L being Linear_Combination of At such that
A4: x = Sum L by RLVECT_3:14;
reconsider L1 = L as Linear_Combination of REAL-NS n by Th11;
( Carrier L1 = Carrier L & Carrier L c= At ) by RLVECT_2:def 6;
then A5: L1 is Linear_Combination of Ar by A1, RLVECT_2:def 6;
Sum L1 = Sum L by Th23;
then x in Lin Ar by A4, A5, RLVECT_3:14;
hence x in [#] (Lin Ar) ; :: thesis: verum