let K be Field; :: thesis: for V being VectSp of K
for W1 being Subspace of V
for L1 being Linear_Combination of W1 ex K1 being Linear_Combination of V st
( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )
let V be VectSp of K; :: thesis: for W1 being Subspace of V
for L1 being Linear_Combination of W1 ex K1 being Linear_Combination of V st
( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )
let W1 be Subspace of V; :: thesis: for L1 being Linear_Combination of W1 ex K1 being Linear_Combination of V st
( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )
let L1 be Linear_Combination of W1; :: thesis: ex K1 being Linear_Combination of V st
( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )
defpred S₁[ set , set ] means ( ( $1 in W1 & $2 = L1 . $1 ) or ( not $1 in W1 & $2 = 0. K ) );
A1: for x being set st x in the carrier of V holds
ex y being set st
( y in the carrier of K & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in the carrier of V implies ex y being set st
( y in the carrier of K & S₁[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being set st
( y in the carrier of K & S₁[x,y] )

per cases ( x in W1 or not x in W1 ) ;

suppose A2: x in W1 ; :: thesis: ex y being set st
( y in the carrier of K & S₁[x,y] )

then reconsider x = x as Vector of W1 by STRUCT_0:def 5;
S₁[x,L1 . x] by A2;
hence ex y being set st
( y in the carrier of K & S₁[x,y] ) ; :: thesis: verum

end;

suppose not x in W1 ; :: thesis: ex y being set st
( y in the carrier of K & S₁[x,y] )

hence ex y being set st
( y in the carrier of K & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

consider K1 being Function of V,K such that
A3: for x being set st x in the carrier of V holds
S₁[x,K1 . x] from FUNCT_2:sch 1(A1);
A4: the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider C = Carrier L1 as finite Subset of V by XBOOLE_1:1;

A5: now

let v be Vector of V; :: thesis: ( not v in C implies K1 . v = 0. K )
assume A6: not v in C ; :: thesis: K1 . v = 0. K
( ( S₁[v,L1 . v] & v in the carrier of W1 ) or S₁[v, 0. K] ) by STRUCT_0:def 5;
then ( ( S₁[v,L1 . v] & L1 . v = 0. K ) or S₁[v, 0. K] ) by A6;
hence K1 . v = 0. K by A3; :: thesis: verum

end;

K1 is Element of Funcs the carrier of V,the carrier of K by FUNCT_2:11;
then reconsider K1 = K1 as Linear_Combination of V by A5, VECTSP_6:def 4;
take K1 ; :: thesis: ( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )

now

let x be set ; :: thesis: ( x in Carrier K1 implies x in the carrier of W1 )
assume A7: ( x in Carrier K1 & not x in the carrier of W1 ) ; :: thesis: contradiction
then consider v being Vector of V such that
A8: ( x = v & K1 . v <> 0. K ) ;
( S₁[v, 0. K] & S₁[v,K1 . v] ) by A3, A7, A8, STRUCT_0:def 5;
hence contradiction by A8; :: thesis: verum

end;

then A9: Carrier K1 c= the carrier of W1 by TARSKI:def 3;
reconsider L' = L1 as Function of W1,K ;
reconsider K' = K1 | the carrier of W1 as Function of the carrier of W1,the carrier of K by A4, FUNCT_2:38;

now

let x be set ; :: thesis: ( x in the carrier of W1 implies L' . x = K' . x )
assume A10: x in the carrier of W1 ; :: thesis: L' . x = K' . x
( S₁[x,L1 . x] & S₁[x,K1 . x] ) by A3, A4, A10, STRUCT_0:def 5;
hence L' . x = K' . x by A10, FUNCT_1:72; :: thesis: verum

end;

then L' = K' by FUNCT_2:18;
hence ( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 ) by A9, VECTSP_9:11; :: thesis: verum