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