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:169;
then A2: dom (l | A) = A by RELAT_1:91;
A3: dom ((V \ A) --> (0. F)) = V \ A by FUNCOP_1:19;
A4: A \/ (([#] V) \ A) = [#] V by XBOOLE_1:45;
A5: dom ((l | A) +* ((V \ A) --> (0. F))) = [#] V by A1, A2, A3, XBOOLE_1:45;
rng ((l | A) +* ((V \ A) --> (0. F))) c= [#] F

proof

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

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

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

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

end;

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

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

end;

end;

end;

then reconsider f = (l | A) +* ((V \ A) --> (0. F)) as Element of Funcs ([#] V),([#] F) by A5, 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 C = Carrier l;
set D = { v where v is Element of V : f . v <> 0. F } ;
{ v where v is Element of V : f . v <> 0. F } is Subset of V

proof

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

proof

let x be set ; :: 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 A12: x in { v where v is Element of V : f . v <> 0. F } ; :: thesis: x in [#] V
consider v being Element of V such that
A13: x = v and
f . v <> 0. F by A12;
thus x in [#] V by A13; :: thesis: verum

end;

hence { v where v is Element of V : f . v <> 0. F } is Subset of V ; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in Carrier l )
assume A14: x in D ; :: thesis: x in Carrier l
consider v being Element of V such that
A15: x = v and
A16: f . v <> 0. F by A14;
A17: dom ((V \ A) --> (0. F)) = V \ A by FUNCOP_1:19;

A18: now

assume A19: v in V \ A ; :: thesis: contradiction
then f . v = ((V \ A) --> (0. F)) . v by A1, A5, A17, FUNCT_4:def 1
.= 0. F by A19, FUNCOP_1:13 ;
hence contradiction by A16; :: thesis: verum

end;

then not v in dom ((V \ A) --> (0. F)) ;
then A20: f . v = (l | A) . v by FUNCT_4:12;
v in A by A18, XBOOLE_0:def 5;
then (l | A) . v = l . v by FUNCT_1:72;
hence x in Carrier l by A15, A16, A20; :: 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 4;
Carrier f c= A

proof

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

now

assume not x in A ; :: thesis: contradiction
then A23: x in V \ A by XBOOLE_0:def 5;
then x in (dom (l | A)) \/ (dom ((V \ A) --> (0. F))) by A3, XBOOLE_0:def 3;
then f . x = ((V \ A) --> (0. F)) . x by A3, A23, FUNCT_4:def 1;
hence contradiction by A22, A23, FUNCOP_1:13; :: 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 7; :: thesis: verum