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) /\ (Carrier L) & 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) /\ (Carrier L) & 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) /\ (Carrier L) & L (#) F = K (#) F )
defpred S₁[ set , set ] means ( not $1 is VECTOR of V or ( $1 in rng F & $2 = L . $1 ) or ( not $1 in rng F & $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 rng F or not x in rng F ) ;

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

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

end;

suppose not x in rng F ; :: 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 K being Function of the carrier of V,REAL st
for x being set st x in the carrier of V holds
S₁[x,K . x] from FUNCT_2:sch 1(A1);
then consider K being Function of the carrier of V,REAL such that
A2: for x being set st x in the carrier of V holds
S₁[x,K . x] ;
reconsider R = rng F as finite Subset of V by FINSEQ_1:def 4;

A3: now

let v be VECTOR of V; :: thesis: ( not v in R /\ (Carrier L) implies K . b₁ = 0 )
assume A4: not v in R /\ (Carrier L) ; :: thesis: K . b₁ = 0

per cases ( not v in R or not v in Carrier L ) by A4, XBOOLE_0:def 4;

suppose not v in R ; :: thesis: K . b₁ = 0

hence K . v = 0 by A2; :: thesis: verum

end;

suppose not v in Carrier L ; :: thesis: K . b₁ = 0

then L . v = 0 by RLVECT_2:28;
hence K . v = 0 by A2; :: thesis: verum

end;

end;

end;

reconsider K = K as Element of Funcs the carrier of V,REAL by FUNCT_2:11;
reconsider K = K as Linear_Combination of V by A3, RLVECT_2:def 5;
take K ; :: thesis: ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F )
A5: Carrier K = (rng F) /\ (Carrier L)

proof

now

let v be set ; :: thesis: ( v in Carrier K implies v in (rng F) /\ (Carrier L) )
assume v in Carrier K ; :: thesis: v in (rng F) /\ (Carrier L)
then v in { v' where v' is VECTOR of V : K . v' <> 0 } by RLVECT_2:def 6;
then consider v' being VECTOR of V such that
A6: ( v' = v & K . v' <> 0 ) ;
thus v in (rng F) /\ (Carrier L) by A3, A6; :: thesis: verum

end;

then A7: Carrier K c= (rng F) /\ (Carrier L) by TARSKI:def 3;

now

let v be set ; :: thesis: ( v in (rng F) /\ (Carrier L) implies v in Carrier K )
assume A8: v in (rng F) /\ (Carrier L) ; :: thesis: v in Carrier K
then A9: ( v in R & v in Carrier L ) by XBOOLE_0:def 4;
reconsider v' = v as VECTOR of V by A8;
( K . v' = L . v' & L . v' <> 0 ) by A2, A9, RLVECT_2:28;
then v in { w where w is VECTOR of V : K . w <> 0 } ;
hence v in Carrier K by RLVECT_2:def 6; :: thesis: verum

end;

then (rng F) /\ (Carrier L) c= Carrier K by TARSKI:def 3;
hence Carrier K = (rng F) /\ (Carrier L) by A7, XBOOLE_0:def 10; :: thesis: verum

end;

L (#) F = K (#) F

proof

set p = L (#) F;
set q = K (#) F;
( len (L (#) F) = len F & len (K (#) F) = len F ) by RLVECT_2:def 9;
then A10: ( dom (L (#) F) = dom (K (#) F) & dom (L (#) F) = dom F ) by FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom (L (#) F) implies (L (#) F) . k = (K (#) F) . k )
assume A11: k in dom (L (#) F) ; :: thesis: (L (#) F) . k = (K (#) F) . k
set u = F /. k;
F /. k = F . k by A10, A11, PARTFUN1:def 8;
then A12: ( S₁[F /. k,K . (F /. k)] & S₁[F /. k,L . (F /. k)] ) by A2, A10, A11, FUNCT_1:def 5;
( (L (#) F) . k = (L . (F /. k)) * (F /. k) & (K (#) F) . k = (K . (F /. k)) * (F /. k) ) by A10, A11, RLVECT_2:def 9;
hence (L (#) F) . k = (K (#) F) . k by A12; :: thesis: verum

end;

hence L (#) F = K (#) F by A10, FINSEQ_1:17; :: thesis: verum

end;

hence ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) by A5; :: thesis: verum