let T be RealLinearSpace; :: thesis: for Af being Subset of (RLSp2RVSp T)
for Ar being Subset of T st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
let Af be Subset of (RLSp2RVSp T); :: thesis: for Ar being Subset of T st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)
let Ar be Subset of T; :: 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 RLSp2RVSp T by Th72;
( Carrier L1 = Carrier L & Carrier L c= Ar ) by Th73, RLVECT_2:def 6;
then A3: L1 is Linear_Combination of Af by A1, VECTSP_6:def 4;
Sum L1 = Sum L by Th76;
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 T by Th72;
( Carrier L1 = Carrier L & Carrier L c= Af ) by Th73, VECTSP_6:def 4;
then A5: L1 is Linear_Combination of Ar by A1, RLVECT_2:def 6;
Sum L1 = Sum L by Th76;
then x in Lin Ar by A4, A5, RLVECT_3:14;
hence x in [#] (Lin Ar) ; :: thesis: verum