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 ;
( 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 ;
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:
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
.= 0. R by ;
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 ; :: 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 ;
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