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

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

hence
L (#) F = (dom F) --> (0. V)
by FUNCOP_1:11, p1; :: thesis: verum
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;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