let GF be Field; :: thesis: for V being VectSp of GF
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 V be VectSp of GF; :: 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₁[ 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. GF ) );
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 the carrier of GF & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st
( y in the carrier of GF & S₁[x,y] ) )
assume x in the carrier of V ; :: thesis: ex y being object st
( y in the carrier of GF & S₁[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 the carrier of GF & S₁[x,y] )

then S₁[x,L . x9] ;
hence ex y being object st
( y in the carrier of GF & S₁[x,y] ) ; :: thesis: verum

end;

suppose not x in rng F ; :: thesis: ex y being object st
( y in the carrier of GF & S₁[x,y] )

hence ex y being object st
( y in the carrier of GF & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

ex K being Function of the carrier of V, the carrier of GF st
for x being object 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, the carrier of GF such that
A2: for x being object st x in the carrier of V holds
S₁[x,K . x] ;

A3: now :: thesis: for v being Vector of V st not v in R /\ (Carrier L) holds
K . v = 0. GF

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

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. GF

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

end;

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

( ( S₁[v,K . v] & S₁[v,L . v] ) or ( S₁[v,K . v] & S₁[v, 0. GF] ) ) by A2;
hence K . v = 0. GF by A5, VECTSP_6:2; :: thesis: verum

end;

end;

end;

reconsider K = K as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
reconsider K = K as Linear_Combination of V by A3, VECTSP_6:def 1;

now :: thesis: for v being object st v in (rng F) /\ (Carrier L) holds
v in Carrier K

let v be object ; :: thesis: ( v in (rng F) /\ (Carrier L) implies v in Carrier K )
assume A6: v in (rng F) /\ (Carrier L) ; :: thesis: v in Carrier K
then reconsider v9 = v as Vector of V ;
v in Carrier L by A6, XBOOLE_0:def 4;
then A7: L . v9 <> 0. GF by VECTSP_6:2;
v in R by A6, XBOOLE_0:def 4;
then K . v9 = L . v9 by A2;
hence v in Carrier K by A7, VECTSP_6:1; :: thesis: verum

end;

then A8: (rng F) /\ (Carrier L) c= Carrier K ;
take K ; :: thesis: ( Carrier K = (rng F) /\ (Carrier L) & 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 VECTSP_6:def 5;
len (K (#) F) = len F by VECTSP_6:def 5;
then A11: dom (L (#) F) = dom (K (#) F) by A10, FINSEQ_3:29;
A12: dom (L (#) F) = dom F by A10, FINSEQ_3:29;

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: S₁[F /. k,K . (F /. k)] by A2;
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 A12, PARTFUN1:def 6, VECTSP_6:def 5;
hence (L (#) F) . k = (K (#) F) . k by A11, A12, A14, A13, FUNCT_1:def 3, VECTSP_6:def 5; :: thesis: verum

end;

hence L (#) F = K (#) F by A11, FINSEQ_1:13; :: thesis: verum

end;

now :: thesis: for v being object st v in Carrier K holds
v in (rng F) /\ (Carrier L)

let v be object ; :: 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 ex v9 being Vector of V st
( v9 = v & K . v9 <> 0. GF ) by VECTSP_6:1;
hence v in (rng F) /\ (Carrier L) by A3; :: thesis: verum

end;

then Carrier K c= (rng F) /\ (Carrier L) ;
hence ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) by A8, A9, XBOOLE_0:def 10; :: thesis: verum