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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((l | A) +* ((V \ A) --> (0. F))) or y in [#] F )
assume y in rng ((l | A) +* ((V \ A) --> (0. F))) ; :: thesis: y in [#] F
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;

per cases ( x in A or x in V \ A ) by A5, XBOOLE_0:def 3;

suppose A8: x in A ; :: thesis: y in [#] F

then not x in dom ((V \ A) --> (0. F)) by XBOOLE_0:def 5;
then A9: ((l | A) +* ((V \ A) --> (0. F))) . x = (l | A) . x by FUNCT_4:11;
(l | A) . x = l . x by A8, FUNCT_1:49;
hence y in [#] F by A7, A9; :: thesis: verum

end;

suppose A10: x in V \ A ; :: thesis: y in [#] F

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: verum

end;

end;

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

proof

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

proof

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

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

proof

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

A14: now :: thesis: not v in V \ A

assume A15: v in V \ A ; :: thesis: contradiction
then f . v = ((V \ A) --> (0. F)) . v by A1, A4, FUNCT_4:def 1
.= 0. F by A15, FUNCOP_1:7 ;
hence contradiction by A12; :: thesis: verum

end;

then v in A by XBOOLE_0:def 5;
then A16: (l | A) . v = l . v by FUNCT_1:49;
not v in dom ((V \ A) --> (0. F)) by A14;
then f . v = (l | A) . v by FUNCT_4:11;
hence x in Carrier l by A11, A12, A16; :: thesis: verum

end;

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

end;

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

proof

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

now :: thesis: x in A

assume not x in A ; :: thesis: contradiction
then A19: x in V \ A by XBOOLE_0:def 5;
then x in (dom (l | A)) \/ (dom ((V \ A) --> (0. F))) by XBOOLE_0:def 3;
then f . x = ((V \ A) --> (0. F)) . x by A19, FUNCT_4:def 1;
hence contradiction by A18, A19, FUNCOP_1:7; :: thesis: verum

end;

hence x in A ; :: thesis: verum

end;

hence (l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A by VECTSP_6:def 4; :: thesis: verum