let R be Ring; :: thesis: for V being LeftMod of R

for l being Linear_Combination of V

for X being Subset of V holds l .: X is finite

let V be LeftMod of R; :: thesis: for l being Linear_Combination of V

for X being Subset of V holds l .: X is finite

let l be Linear_Combination of V; :: thesis: for X being Subset of V holds l .: X is finite

let X be Subset of V; :: thesis: l .: X is finite

A1: l = l ! (Carrier l) by Th24;

(rng (l | (Carrier l))) \/ (rng (((Carrier l) `) --> (0. R))) is finite ;

then rng l is finite by A1, FINSET_1:1, FUNCT_4:17;

hence l .: X is finite by FINSET_1:1, RELAT_1:111; :: thesis: verum

for l being Linear_Combination of V

for X being Subset of V holds l .: X is finite

let V be LeftMod of R; :: thesis: for l being Linear_Combination of V

for X being Subset of V holds l .: X is finite

let l be Linear_Combination of V; :: thesis: for X being Subset of V holds l .: X is finite

let X be Subset of V; :: thesis: l .: X is finite

A1: l = l ! (Carrier l) by Th24;

(rng (l | (Carrier l))) \/ (rng (((Carrier l) `) --> (0. R))) is finite ;

then rng l is finite by A1, FINSET_1:1, FUNCT_4:17;

hence l .: X is finite by FINSET_1:1, RELAT_1:111; :: thesis: verum