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: rng ((V \ (Carrier l)) --> (0. F)) c= {(0. F)}

proof

set f = (V \ (Carrier l)) --> (0. F);

per cases ( V \ (Carrier l) = {} or V \ (Carrier l) <> {} ) ;

suppose V \ (Carrier l) = {} ; :: thesis: rng ((V \ (Carrier l)) --> (0. F)) c= {(0. F)}

then (V \ (Carrier l)) --> (0. F) = {} ;
hence rng ((V \ (Carrier l)) --> (0. F)) c= {(0. F)} by RELAT_1:60, XBOOLE_1:2; :: thesis: verum

end;

suppose V \ (Carrier l) <> {} ; :: thesis: rng ((V \ (Carrier l)) --> (0. F)) c= {(0. F)}

hence rng ((V \ (Carrier l)) --> (0. F)) c= {(0. F)} by FUNCOP_1:14; :: thesis: verum

end;

end;

end;

A2: l = l ! (Carrier l) by Th24;
(rng (l | (Carrier l))) \/ (rng ((V \ (Carrier l)) --> (0. F))) is finite by A1;
then rng l is finite by A2, FINSET_1:13, FUNCT_4:18;
hence l .: X is finite by FINSET_1:13, RELAT_1:144; :: thesis: verum