let K be Field; :: thesis: for V being VectSp of K
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 V be VectSp of K; :: 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 VECTSP_4:def 2;
then L | the carrier of W is Function of the carrier of W, the carrier of K by FUNCT_2:32;
then reconsider L1 = L | the carrier of W as Element of Funcs ( the carrier of W, the carrier of K) 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. K
proof
let v be Element of W; :: thesis: ( not v in (Carrier L) /\ the carrier of W implies L1 . v = 0. K )
reconsider w = v as Element of V by VECTSP_4:10;
assume not v in (Carrier L) /\ the carrier of W ; :: thesis: L1 . v = 0. K
then A2: not v in Carrier L by XBOOLE_0:def 4;
L . w = L1 . v by FUNCT_1:49;
hence L1 . v = 0. K by A2, VECTSP_6:2; :: 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, VECTSP_6:def 1; :: thesis: verum