let V be RealUnitarySpace; 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; 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; ex L being Linear_Combination of V st
( Carrier K = Carrier L & Sum K = Sum L )
defpred S1[ 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 RUSUB_1:def 1;
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 & S1[x,y] )
ex L being Function of the carrier of V,REAL st
for x being object st x in the carrier of V holds
S1[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
S1[x,L . x]
;
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
; ( Carrier K = Carrier L & Sum K = Sum L )
then A7:
Carrier L c= the carrier of W
;
then
K9 = L9
by FUNCT_2:12;
hence
( Carrier K = Carrier L & Sum K = Sum L )
by A7, Th18; verum