set f = (l | A) +* ((V \ A) --> (0. F));
A1: dom ((l | A) +* ((V \ A) --> (0. F))) = (dom (l | A)) \/ (dom ((V \ A) --> (0. F))) by FUNCT_4:def 1;
dom l = [#] V by FUNCT_2:92;
then A3: dom (l | A) = A by RELAT_1:62;
then A4: dom ((l | A) +* ((V \ A) --> (0. F))) = [#] V by A1, XBOOLE_1:45;
A5: A \/ (([#] V) \ A) = [#] V by XBOOLE_1:45;
rng ((l | A) +* ((V \ A) --> (0. F))) c= [#] F

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ((l | A) +* ((V \ A) --> (0. F))) ; :: thesis:
then consider x being object such that
A6: x in dom ((l | A) +* ((V \ A) --> (0. F))) and
A7: y = ((l | A) +* ((V \ A) --> (0. F))) . x by FUNCT_1:def 3;
reconsider x = x as Element of V by A1, A3, A6, XBOOLE_1:45;

end;

then x in dom ((V \ A) --> (0. F)) ;
then ((l | A) +* ((V \ A) --> (0. F))) . x = ((V \ A) --> (0. F)) . x by FUNCT_4:13
.= 0. F by A10, FUNCOP_1:7 ;
hence y in [#] F by A7; :: thesis:

end;

then reconsider f = (l | A) +* ((V \ A) --> (0. F)) as Element of Funcs (([#] V),([#] F)) by A4, FUNCT_2:def 2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds
f . v = 0. F

set D = { v where v is Element of V : f . v <> 0. F } ;
{ v where v is Element of V : f . v <> 0. F } c= [#] V

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { v where v is Element of V : f . v <> 0. F } ; :: thesis:
then ex v being Element of V st
( x = v & f . v <> 0. F ) ;
hence x in [#] V ; :: thesis:

end;

then reconsider D = { v where v is Element of V : f . v <> 0. F } as Subset of V ;
set C = Carrier l;
D c= Carrier l

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in D ; :: thesis:
then consider v being Element of V such that
A11: x = v and
A12: f . v <> 0. F ;

end;

end;

then reconsider D = D as finite Subset of V ;
take D ; :: thesis:
thus for v being Element of V st not v in D holds
f . v = 0. F ; :: thesis:

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
Carrier f c= A

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A17: x in Carrier f ; :: thesis:
reconsider x = x as Element of V by A17;
A18: f . x <> 0. F by A17, VECTSP_6:2;

end;

end;