let F be Field; :: thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
let V be VectSp of F; :: 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 ((V \ (Carrier l)) --> (0. F))) 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