set f = (l | A) +* ((A `) --> (0. R));
A1: dom ((l | A) +* ((A `) --> (0. R))) = (dom (l | A)) \/ (dom ((A `) --> (0. R))) by FUNCT_4:def 1;
dom l = [#] V by FUNCT_2:92;
then dom (l | A) = A by RELAT_1:62;
then A4: dom ((l | A) +* ((A `) --> (0. R))) = [#] V by A1, XBOOLE_1:45;
( rng ((l | A) +* ((A `) --> (0. R))) c= (rng (l | A)) \/ (rng ((A `) --> (0. R))) & (rng (l | A)) \/ (rng ((A `) --> (0. R))) c= [#] R ) by FUNCT_4:17;
then rng ((l | A) +* ((A `) --> (0. R))) c= the carrier of R ;
then reconsider f = (l | A) +* ((A `) --> (0. R)) as Element of Funcs (([#] V), the carrier of R) 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. R

proof

set D = { v where v is Element of V : f . v <> 0. R } ;
{ v where v is Element of V : f . v <> 0. R } 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. R } or x in [#] V )
assume x in { v where v is Element of V : f . v <> 0. R } ; :: thesis: x in [#] V
then ex v being Element of V st
( x = v & f . v <> 0. R ) ;
hence x in [#] V ; :: thesis: verum

end;

then reconsider D = { v where v is Element of V : f . v <> 0. R } 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
A10: x = v and
A11: f . v <> 0. R ;

A13: now :: thesis: not v in A `

assume A14: v in A ` ; :: thesis: contradiction
then f . v = ((A `) --> (0. R)) . v by A1, A4, FUNCT_4:def 1
.= 0. R by A14, FUNCOP_1:7 ;
hence contradiction by A11; :: thesis: verum

end;

then v in A by XBOOLE_0:def 5;
then A15: (l | A) . v = l . v by FUNCT_1:49;
not v in dom ((A `) --> (0. R)) by A13;
then f . v = (l | A) . v by FUNCT_4:11;
hence x in Carrier l by A10, A11, A15; :: 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. R
thus for v being Element of V st not v in D holds
f . v = 0. R ; :: 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 A16: x in Carrier f ; :: thesis: x in A
reconsider x = x as Element of V by A16;

now :: thesis: x in A

assume not x in A ; :: thesis: contradiction
then A17: x in A ` by XBOOLE_0:def 5;
then x in (dom (l | A)) \/ (dom ((A `) --> (0. R))) by XBOOLE_0:def 3;
then f . x = ((A `) --> (0. R)) . x by A17, FUNCT_4:def 1;
hence contradiction by A16, A17, FUNCOP_1:7, VECTSP_6:2; :: thesis: verum

end;

hence x in A ; :: thesis: verum

end;

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