let F be Field; :: thesis: for U, V being VectSp of F
for B being non empty finite Subset of U st B is linearly-independent holds
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w
let U, V be VectSp of F; :: thesis: for B being non empty finite Subset of U st B is linearly-independent holds
for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w
let B be non empty finite Subset of U; :: thesis: ( B is linearly-independent implies for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w )
assume AS1: B is linearly-independent ; :: thesis: for w being Element of U st w in B holds
for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w
let w be Element of U; :: thesis: ( w in B implies for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w )
assume AS2: w in B ; :: thesis: for l being Linear_Combination of B st Sum l = w holds
for f being Function of B,V holds Sum (f (#) l) = f . w
let l be Linear_Combination of B; :: thesis: ( Sum l = w implies for f being Function of B,V holds Sum (f (#) l) = f . w )
assume AS3: Sum l = w ; :: thesis: for f being Function of B,V holds Sum (f (#) l) = f . w
let f be Function of B,V; :: thesis: Sum (f (#) l) = f . w
set G = f (#) l;
reconsider b = w as Element of B by AS2;
I: ( Carrier l = {w} & l . w = 1. F ) by AS1, AS2, AS3, lembas1;
then Sum (f (#) l) = (l . b) * (f . b) by lemadd2;
hence Sum (f (#) l) = f . w by I; :: thesis: verum