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

Carrier f c= A

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

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
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

set C = Carrier l;

D c= Carrier l

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;{ v where v is Element of V : f . v <> 0. R } c= [#] V

proof

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

set C = Carrier l;

D c= Carrier l

proof

then reconsider D = D as finite Subset of V ;
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 ;

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;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 `

then
v in A
by XBOOLE_0:def 5;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 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

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

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

Carrier f c= A

proof

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

end;assume A16: x in Carrier f ; :: thesis: x in A

reconsider x = x as Element of V by A16;

now :: thesis: x in A

hence
x in A
; :: thesis: verumassume
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;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