let V be Z_Module; :: thesis:
let L be Linear_Combination of V; :: thesis:
let F be FinSequence of V; :: thesis:
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 ) );
reconsider R = rng F as finite Subset of V ;
A1: for x being object st x in the carrier of V holds
ex y being object st
( y in INT & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of V ; :: thesis:
then reconsider x9 = x as Vector of V ;

per cases ;

suppose A2: x in rng F ; :: thesis:

L . x9 in INT ;
hence ex y being object st
( y in INT & S₁[x,y] ) by A2; :: thesis:

end;

suppose A3: not x in rng F ; :: thesis:

thus ex y being object st
( y in INT & S₁[x,y] ) by A3; :: thesis:

end;

end;

end;

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

A5: now :: thesis:

let v be Vector of V; :: thesis:
assume A6: not v in R /\ (Carrier L) ; :: thesis:

per cases by A6, XBOOLE_0:def 4;

suppose not v in R ; :: thesis:

hence K . v = 0 by A4; :: thesis:

end;

suppose not v in Carrier L ; :: thesis:

then L . v = 0 ;
hence K . v = 0 by A4; :: thesis:

end;

end;

end;

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

now :: thesis:

let v be object ; :: thesis:
assume A7: v in (rng F) /\ (Carrier L) ; :: thesis:
then reconsider v9 = v as Vector of V ;
v in Carrier L by A7, XBOOLE_0:def 4;
then A8: L . v9 <> 0 by ZMODUL02:8;
v in R by A7, XBOOLE_0:def 4;
then K . v9 = L . v9 by A4;
hence v in Carrier K by A8; :: thesis:

end;

then A9: (rng F) /\ (Carrier L) c= Carrier K ;
take K ; :: thesis:
A10: L (#) F = K (#) F

proof

set p = L (#) F;
set q = K (#) F;
A11: len (L (#) F) = len F by VECTSP_6:def 5;
len (K (#) F) = len F by VECTSP_6:def 5;
then A12: dom (L (#) F) = dom (K (#) F) by A11, FINSEQ_3:29;
A13: dom (L (#) F) = dom F by A11, FINSEQ_3:29;

now :: thesis:

let k be Nat; :: thesis:
set u = F /. k;
A14: S₁[F /. k,K . (F /. k)] by A4;
assume A15: k in dom (L (#) F) ; :: thesis:
then ( F /. k = F . k & (L (#) F) . k = (L . (F /. k)) * (F /. k) ) by A13, PARTFUN1:def 6, VECTSP_6:def 5;
hence (L (#) F) . k = (K (#) F) . k by A12, A13, A15, A14, FUNCT_1:def 3, VECTSP_6:def 5; :: thesis:

end;

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

end;

now :: thesis:

let v be object ; :: thesis:
assume v in Carrier K ; :: thesis:
then ex v9 being Vector of V st
( v9 = v & K . v9 <> 0 ) ;
hence v in (rng F) /\ (Carrier L) by A5; :: thesis:

end;

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