let n be Nat; :: thesis: for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
set V = n -VectSp_over F_Real;
set T = TOP-REAL n;
let Af be Subset of (n -VectSp_over F_Real); :: thesis: for Ar being Subset of (TOP-REAL n) st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
let Ar be Subset of (TOP-REAL n); :: thesis: ( Af = Ar implies [#] (Lin Ar) = [#] (Lin Af) )
assume A1: Af = Ar ; :: thesis: [#] (Lin Ar) = [#] (Lin Af)

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

let x be object ; :: thesis: ( x in [#] (Lin Ar) implies x in [#] (Lin Af) )
assume x in [#] (Lin Ar) ; :: thesis: x in [#] (Lin Af)
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 n -VectSp_over F_Real by Th1;
( Carrier L1 = Carrier L & Carrier L c= Ar ) by Th2, RLVECT_2:def 6;
then A3: L1 is Linear_Combination of Af by A1, VECTSP_6:def 4;
Sum L1 = Sum L by Th5;
then x in Lin Af by A2, A3, VECTSP_7:7;
hence x in [#] (Lin Af) ; :: thesis: verum

end;

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