let F be Field; :: thesis: for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l being Linear_Combination of B
for v being Element of V st not v in rng f holds
(f (#) l) . v = 0. F
let U, V be VectSp of F; :: thesis: for B being non empty finite Subset of U
for f being Function of B,V
for l being Linear_Combination of B
for v being Element of V st not v in rng f holds
(f (#) l) . v = 0. F
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V
for l being Linear_Combination of B
for v being Element of V st not v in rng f holds
(f (#) l) . v = 0. F
let f be Function of B,V; :: thesis: for l being Linear_Combination of B
for v being Element of V st not v in rng f holds
(f (#) l) . v = 0. F
let l be Linear_Combination of B; :: thesis: for v being Element of V st not v in rng f holds
(f (#) l) . v = 0. F
let v be Element of V; :: thesis: ( not v in rng f implies (f (#) l) . v = 0. F )
assume B1: not v in rng f ; :: thesis: (f (#) l) . v = 0. F

now :: thesis: for o being object holds not o in {v} /\ (rng f)

let o be object ; :: thesis: not o in {v} /\ (rng f)
assume o in {v} /\ (rng f) ; :: thesis: contradiction
then ( o in {v} & o in rng f ) by XBOOLE_0:def 4;
hence contradiction by B1, TARSKI:def 1; :: thesis: verum

end;

then {v} misses rng f by XBOOLE_0:def 1;
then f " {v} = {} by RELAT_1:138;
then Expand (f,l,v) = <*> the carrier of F ;
then Sum (Expand (f,l,v)) = 0. F by RLVECT_1:43;
hence (f (#) l) . v = 0. F by defK; :: thesis: verum