let F be Field; :: thesis:
let U, V be VectSp of F; :: thesis:
let B be non empty finite Subset of U; :: thesis:
let b be Element of B; :: thesis:
let f be Function of B,V; :: thesis:
let l be Linear_Combination of B; :: thesis:
assume A: Carrier l = {b} ; :: thesis:
H: dom f = B by FUNCT_2:def 1;
then reconsider v = f . b as Element of rng f by FUNCT_1:3;
F: b in Carrier l by A, TARSKI:def 1;
set T = Expand (f,l,v);
f . b in {v} by TARSKI:def 1;
then b in f " {v} by H, FUNCT_1:def 7;
then b in rng (canFS (f " {v})) by FUNCT_2:def 3;
then consider i being object such that
E: ( i in dom (canFS (f " {v})) & (canFS (f " {v})) . i = b ) by FUNCT_1:def 3;
reconsider i = i as Element of NAT by E;
K: dom l = the carrier of U by FUNCT_2:def 1;
then L: i in dom (Expand (f,l,v)) by E, FUNCT_1:11;
G: l . b = (l * (canFS (f " {v}))) . i by E, FUNCT_1:13
.= (Expand (f,l,v)) /. i by L, PARTFUN1:def 6 ;

end;

C: (f (#) l) . v = Sum (Expand (f,l,v)) by defK
.= l . b by G, K, I, E, FUNCT_1:11, POLYNOM2:3 ;

end;

let o be object ; :: thesis:
assume o in Carrier (f (#) l) ; :: thesis:
then consider v being Element of V such that
B0: ( o = v & (f (#) l) . v <> 0. F ) ;
B1: f .: {b} = Im (f,b)
.= {(f . b)} by H, FUNCT_1:59 ;
B2: Carrier (f (#) l) c= f .: {b} by A, lemadd2a;

end;

end;