let K be Ring; :: thesis: for V being LeftMod of K
for L being Linear_Combination of V
for F being FinSequence of V st (rng F) /\ (Carrier L) = {} holds
L (#) F = (dom F) --> (0. V)
let V be LeftMod of K; :: thesis: for L being Linear_Combination of V
for F being FinSequence of V st (rng F) /\ (Carrier L) = {} holds
L (#) F = (dom F) --> (0. V)
let L be Linear_Combination of V; :: thesis: for F being FinSequence of V st (rng F) /\ (Carrier L) = {} holds
L (#) F = (dom F) --> (0. V)
let F be FinSequence of V; :: thesis: ( (rng F) /\ (Carrier L) = {} implies L (#) F = (dom F) --> (0. V) )
assume AS: (rng F) /\ (Carrier L) = {} ; :: thesis: L (#) F = (dom F) --> (0. V)
P1: len (L (#) F) = len F by VECTSP_6:def 5;
then p1: dom (L (#) F) = dom F by FINSEQ_3:29;
for z being object st z in dom (L (#) F) holds
(L (#) F) . z = 0. V

proof

let z be object ; :: thesis: ( z in dom (L (#) F) implies (L (#) F) . z = 0. V )
assume X1: z in dom (L (#) F) ; :: thesis: (L (#) F) . z = 0. V
then reconsider i = z as Nat ;
X3: i in dom F by X1, P1, FINSEQ_3:29;
then F . i in rng F by FUNCT_1:3;
then X4: not F . i in Carrier L by XBOOLE_0:def 4, AS;
F /. i = F . i by X3, PARTFUN1:def 6;
then L . (F /. i) = 0. K by X4;
hence (L (#) F) . z = (0. K) * (F /. i) by X1, VECTSP_6:def 5
.= 0. V by VECTSP_1:14 ;
:: thesis: verum

end;

hence L (#) F = (dom F) --> (0. V) by FUNCOP_1:11, p1; :: thesis: verum