let X be RealLinearSpace; :: thesis: [#] (Lin ([#] X)) = [#] X
for x being object holds
( x in [#] (Lin ([#] X)) iff x in [#] X )

proof

let x be object ; :: thesis: ( x in [#] (Lin ([#] X)) iff x in [#] X )

hereby :: thesis: ( x in [#] X implies x in [#] (Lin ([#] X)) )

assume x in [#] (Lin ([#] X)) ; :: thesis: x in [#] X
then ex l being Linear_Combination of [#] X st x = Sum l by RLVECT_3:14, STRUCT_0:def 5;
hence x in [#] X ; :: thesis: verum

end;

assume x in [#] X ; :: thesis: x in [#] (Lin ([#] X))
then reconsider v = x as Point of X ;
consider l being Linear_Combination of X such that
A1: ( l . v = 1 & Carrier l = {v} ) by Th5;
A2: Sum l = (l . v) * v by A1, RLVECT_2:35
.= v by RLVECT_1:def 8, A1 ;
Carrier l c= [#] X ;
then reconsider l = l as Linear_Combination of [#] X by RLVECT_2:def 6;
x = Sum l by A2;
hence x in [#] (Lin ([#] X)) by STRUCT_0:def 5, RLVECT_3:14; :: thesis: verum

end;

hence [#] (Lin ([#] X)) = [#] X by TARSKI:2; :: thesis: verum