let V be RealLinearSpace; :: thesis: for W being Subspace of V
for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
let W be Subspace of V; :: thesis: for L being Linear_Combination of V holds L | the carrier of W is Linear_Combination of W
let L be Linear_Combination of V; :: thesis: L | the carrier of W is Linear_Combination of W
set cW = the carrier of W;
the carrier of W c= [#] V by RLSUB_1:def 2;
then L | the carrier of W is Function of the carrier of W,REAL by FUNCT_2:32;
then reconsider L1 = L | the carrier of W as Element of Funcs ( the carrier of W,REAL) by FUNCT_2:8;
A1: for v being Element of W st not v in (Carrier L) /\ the carrier of W holds
L1 . v = 0

proof

let v be Element of W; :: thesis: ( not v in (Carrier L) /\ the carrier of W implies L1 . v = 0 )
reconsider w = v as Element of V by RLSUB_1:10;
assume not v in (Carrier L) /\ the carrier of W ; :: thesis: L1 . v = 0
then A2: not v in Carrier L by XBOOLE_0:def 4;
L . w = L1 . v by FUNCT_1:49;
hence L1 . v = 0 by A2, RLVECT_2:19; :: thesis: verum

end;

(Carrier L) /\ the carrier of W c= the carrier of W by XBOOLE_1:17;
hence L | the carrier of W is Linear_Combination of W by A1, RLVECT_2:def 3; :: thesis: verum