let GF be Field; :: thesis: for V being VectSp of GF
for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let V be VectSp of GF; :: thesis: for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let W be Subspace of V; :: thesis: for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
let L be Linear_Combination of V; :: thesis: ( Carrier L c= the carrier of W implies ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L ) )
assume A1: Carrier L c= the carrier of W ; :: thesis: ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )
then reconsider C = Carrier L as finite Subset of W ;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider K = L | the carrier of W as Function of the carrier of W, the carrier of GF by FUNCT_2:32;
A2: K is Element of Funcs ( the carrier of W, the carrier of GF) by FUNCT_2:8;
A3: dom K = the carrier of W by FUNCT_2:def 1;
now :: thesis: for w being Vector of W st not w in C holds
K . w = 0. GF
let w be Vector of W; :: thesis: ( not w in C implies K . w = 0. GF )
A4: w is Vector of V by VECTSP_4:10;
assume not w in C ; :: thesis: K . w = 0. GF
then L . w = 0. GF by A4, VECTSP_6:2;
hence K . w = 0. GF by A3, FUNCT_1:47; :: thesis: verum
end;
then reconsider K = K as Linear_Combination of W by A2, VECTSP_6:def 1;
take K ; :: thesis: ( Carrier K = Carrier L & Sum K = Sum L )
thus ( Carrier K = Carrier L & Sum K = Sum L ) by A1, Th7; :: thesis: verum