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) /\ () = {} 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) /\ () = {} holds
L (#) F = (dom F) --> (0. V)

let L be Linear_Combination of V; :: thesis: for F being FinSequence of V st (rng F) /\ () = {} holds
L (#) F = (dom F) --> (0. V)

let F be FinSequence of V; :: thesis: ( (rng F) /\ () = {} implies L (#) F = (dom F) --> (0. V) )
assume AS: (rng F) /\ () = {} ; :: 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 ;
then F . i in rng F by FUNCT_1:3;
then X4: not F . i in Carrier L by ;
F /. i = F . i by ;
then L . (F /. i) = 0. K by X4;
hence (L (#) F) . z = (0. K) * (F /. i) by
.= 0. V by VECTSP_1:14 ;
:: thesis: verum
end;
hence L (#) F = (dom F) --> (0. V) by ; :: thesis: verum