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

proof

let x be set ; :: thesis: ( x in the carrier of V implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
then reconsider x = x as VECTOR of V ;

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

suppose A2: x in W ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )

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

end;

suppose not x in W ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )

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

end;

end;

end;

ex L being Function of the carrier of V,REAL st
for x being set st x in the carrier of V holds
S₁[x,L . x] from FUNCT_2:sch 1(A1);
then consider L being Function of the carrier of V,REAL such that
A3: for x being set st x in the carrier of V holds
S₁[x,L . x] ;
A4: 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;

A5: now

let v be VECTOR of V; :: thesis: ( not v in C implies L . v = 0 )
assume not v in C ; :: thesis: L . v = 0
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:28;
hence L . v = 0 by A3; :: thesis: verum

end;

L is Element of Funcs the carrier of V,REAL by FUNCT_2:11;
then reconsider L = L as Linear_Combination of V by A5, RLVECT_2:def 5;
take L ; :: thesis: ( Carrier K = Carrier L & Sum K = Sum L )

now

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

end;

then A8: Carrier L c= the carrier of W by TARSKI:def 3;
reconsider K' = K as Function of the carrier of W,REAL ;
reconsider L' = L | the carrier of W as Function of the carrier of W,REAL by A4, FUNCT_2:38;

now

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

end;

then K' = L' by FUNCT_2:18;
hence ( Carrier K = Carrier L & Sum K = Sum L ) by A8, Th11; :: thesis: verum