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₁[ object , object ] means ( ( $1 in W1 & $2 = L1 . $1 ) or ( not $1 in W1 & $2 = 0. K ) );
reconsider L9 = L1 as Function of W1,K ;
A1: for x being object st x in the carrier of V holds
ex y being object st
( y in the carrier of K & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of K & S₁[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being object 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 object st
( y in the carrier of K & S₁[x,y] )

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

end;

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

hence ex y being object 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 object 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 :: thesis: for v being Vector of V st not v in C holds
K1 . v = 0. K

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:8;
then reconsider K1 = K1 as Linear_Combination of V by A5, VECTSP_6:def 1;
reconsider K9 = K1 | the carrier of W1 as Function of the carrier of W1, the carrier of K by A4, FUNCT_2:32;
take K1 ; :: thesis: ( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )

now :: thesis: for x being object st x in Carrier K1 holds
x in the carrier of W1

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

end;

then A11: Carrier K1 c= the carrier of W1 ;

now :: thesis: for x being object st x in the carrier of W1 holds
L9 . x = K9 . x

let x be object ; :: thesis: ( x in the carrier of W1 implies L9 . x = K9 . x )
assume A12: x in the carrier of W1 ; :: thesis: L9 . x = K9 . x
S₁[x,K1 . x] by A3, A4, A12;
hence L9 . x = K9 . x by A12, FUNCT_1:49, STRUCT_0:def 5; :: thesis: verum

end;

then L9 = K9 by FUNCT_2:12;
hence ( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 ) by A11, VECTSP_9:7; :: thesis: verum