let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V
for F being FinSequence of the carrier of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ () & L (#) F = K (#) F )

let L be Linear_Combination of V; :: thesis: for F being FinSequence of the carrier of V ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ () & L (#) F = K (#) F )

let F be FinSequence of the carrier of V; :: thesis: ex K being Linear_Combination of V st
( Carrier K = (rng F) /\ () & L (#) F = K (#) F )

defpred S1[ object , object ] means ( not \$1 is VECTOR of V or ( \$1 in rng F & \$2 = L . \$1 ) or ( not \$1 in rng F & \$2 = 0 ) );
reconsider R = rng F as finite Subset of V by FINSEQ_1:def 4;
A1: for x being object st x in the carrier of V holds
ex y being object st
( y in REAL & S1[x,y] )
proof
A2: 0 in REAL by XREAL_0:def 1;
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in REAL & S1[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )

then reconsider x9 = x as VECTOR of V ;
per cases ( x in rng F or not x in rng F ) ;
suppose x in rng F ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )

then S1[x,L . x9] ;
hence ex y being object st
( y in REAL & S1[x,y] ) by A2; :: thesis: verum
end;
suppose not x in rng F ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )

hence ex y being object st
( y in REAL & S1[x,y] ) by A2; :: thesis: verum
end;
end;
end;
ex K being Function of the carrier of V,REAL st
for x being object st x in the carrier of V holds
S1[x,K . x] from then consider K being Function of the carrier of V,REAL such that
A3: for x being object st x in the carrier of V holds
S1[x,K . x] ;
A4: now :: thesis: for v being VECTOR of V st not v in R /\ () holds
K . v = 0
let v be VECTOR of V; :: thesis: ( not v in R /\ () implies K . b1 = 0 )
assume A5: not v in R /\ () ; :: thesis: K . b1 = 0
per cases ( not v in R or not v in Carrier L ) by ;
end;
end;
reconsider K = K as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
reconsider K = K as Linear_Combination of V by ;
now :: thesis: for v being object st v in (rng F) /\ () holds
v in Carrier K
let v be object ; :: thesis: ( v in (rng F) /\ () implies v in Carrier K )
assume A6: v in (rng F) /\ () ; :: thesis:
then reconsider v9 = v as VECTOR of V ;
v in Carrier L by ;
then A7: L . v9 <> 0 by RLVECT_2:19;
v in R by ;
then K . v9 = L . v9 by A3;
then v in { w where w is VECTOR of V : K . w <> 0 } by A7;
hence v in Carrier K by RLVECT_2:def 4; :: thesis: verum
end;
then A8: (rng F) /\ () c= Carrier K ;
take K ; :: thesis: ( Carrier K = (rng F) /\ () & L (#) F = K (#) F )
A9: L (#) F = K (#) F
proof
set p = L (#) F;
set q = K (#) F;
A10: len (L (#) F) = len F by RLVECT_2:def 7;
len (K (#) F) = len F by RLVECT_2:def 7;
then A11: dom (L (#) F) = dom (K (#) F) by ;
A12: dom (L (#) F) = dom F by ;
now :: thesis: for k being Nat st k in dom (L (#) F) holds
(L (#) F) . k = (K (#) F) . k
let k be Nat; :: thesis: ( k in dom (L (#) F) implies (L (#) F) . k = (K (#) F) . k )
set u = F /. k;
A13: S1[F /. k,K . (F /. k)] by A3;
assume A14: k in dom (L (#) F) ; :: thesis: (L (#) F) . k = (K (#) F) . k
then ( F /. k = F . k & (L (#) F) . k = (L . (F /. k)) * (F /. k) ) by ;
hence (L (#) F) . k = (K (#) F) . k by ; :: thesis: verum
end;
hence L (#) F = K (#) F by ; :: thesis: verum
end;
now :: thesis: for v being object st v in Carrier K holds
v in (rng F) /\ ()
let v be object ; :: thesis: ( v in Carrier K implies v in (rng F) /\ () )
assume v in Carrier K ; :: thesis: v in (rng F) /\ ()
then v in { v9 where v9 is VECTOR of V : K . v9 <> 0 } by RLVECT_2:def 4;
then ex v9 being VECTOR of V st
( v9 = v & K . v9 <> 0 ) ;
hence v in (rng F) /\ () by A4; :: thesis: verum
end;
then Carrier K c= (rng F) /\ () ;
hence ( Carrier K = (rng F) /\ () & L (#) F = K (#) F ) by ; :: thesis: verum