let F be Field; :: thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let V be VectSp of F; :: thesis: for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let l be Linear_Combination of V; :: thesis: for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let X be Subset of V; :: thesis: ( X misses Carrier l implies l .: X c= {(0. F)} )
assume A1: X misses Carrier l ; :: thesis: l .: X c= {(0. F)}
set M = l .: X;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in l .: X or y in {(0. F)} )
assume A2: y in l .: X ; :: thesis: y in {(0. F)}
consider x being set such that
A3: x in dom l and
A4: x in X and
A5: y = l . x by A2, FUNCT_1:def 12;
reconsider x = x as Element of V by A3;

now

assume l . x <> 0. F ; :: thesis: contradiction
then x in Carrier l ;
then x in (Carrier l) /\ X by A4, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence y in {(0. F)} by A5, TARSKI:def 1; :: thesis: verum