let V be RealLinearSpace; :: thesis:
let W be Subspace of V; :: thesis:
let K be Linear_Combination of W; :: thesis:
defpred S₁[ object , object ] means ( ( $1 in W & $2 = K . $1 ) or ( not $1 in W & $2 = 0 ) );
reconsider K9 = K as Function of the carrier of W,REAL ;
A1: the carrier of W c= the carrier of V by RLSUB_1:def 2;
then reconsider C = Carrier K as finite Subset of V by XBOOLE_1:1;
A2: for x being object st x in the carrier of V holds
ex y being object st
( y in REAL & S₁[x,y] )

let x be object ; :: thesis:
assume x in the carrier of V ; :: thesis:
then reconsider x = x as VECTOR of V ;
A3: 0 in REAL by XREAL_0:def 1;

then reconsider x = x as VECTOR of W by STRUCT_0:def 5;
S₁[x,K . x] by A4;
hence ex y being object st
( y in REAL & S₁[x,y] ) ; :: thesis:

end;

end;

ex L being Function of the carrier of V,REAL st
for x being object st x in the carrier of V holds
S₁[x,L . x] from FUNCT_2:sch 1(A2);
then consider L being Function of the carrier of V,REAL such that
A5: for x being object st x in the carrier of V holds
S₁[x,L . x] ;

let v be VECTOR of V; :: thesis:
assume not v in C ; :: thesis:
then ( ( S₁[v,K . v] & not v in C & v in the carrier of W ) or S₁[v, 0 ] ) by STRUCT_0:def 5;
then ( ( S₁[v,K . v] & K . v = 0 ) or S₁[v, 0 ] ) by RLVECT_2:19;
hence L . v = 0 by A5; :: thesis:

end;

L is Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
then reconsider L = L as Linear_Combination of V by A6, RLVECT_2:def 3;
reconsider L9 = L | the carrier of W as Function of the carrier of W,REAL by A1, FUNCT_2:32;
take L ; :: thesis:

end;

end;