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 holds Carrier (f (#) l) c= f .: (Carrier l)
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 holds Carrier (f (#) l) c= f .: (Carrier l)
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V
for l being Linear_Combination of B holds Carrier (f (#) l) c= f .: (Carrier l)
let f be Function of B,V; :: thesis: for l being Linear_Combination of B holds Carrier (f (#) l) c= f .: (Carrier l)
let l be Linear_Combination of B; :: thesis: Carrier (f (#) l) c= f .: (Carrier l)

now :: thesis: for o being object st o in Carrier (f (#) l) holds
o in f .: (Carrier l)

let o be object ; :: thesis: ( o in Carrier (f (#) l) implies o in f .: (Carrier l) )
assume o in Carrier (f (#) l) ; :: thesis: o in f .: (Carrier l)
then consider v being Element of V such that
B1: ( o = v & (f (#) l) . v <> 0. F ) ;
set T = Expand (f,l,v);

now :: thesis: not f " {v} misses Carrier l

assume A3: f " {v} misses Carrier l ; :: thesis: contradiction
set L = (len (Expand (f,l,v))) |-> (0. F);

now :: thesis: for i being Nat st 1 <= i & i <= len (Expand (f,l,v)) holds
(Expand (f,l,v)) . i = ((len (Expand (f,l,v))) |-> (0. F)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (Expand (f,l,v)) implies (Expand (f,l,v)) . i = ((len (Expand (f,l,v))) |-> (0. F)) . i )
assume ( 1 <= i & i <= len (Expand (f,l,v)) ) ; :: thesis: (Expand (f,l,v)) . i = ((len (Expand (f,l,v))) |-> (0. F)) . i
then A6: ( i in dom (Expand (f,l,v)) & i in Seg (len (Expand (f,l,v))) ) by FINSEQ_3:25;
then ( i in dom (canFS (f " {v})) & (canFS (f " {v})) . i in dom l ) by FUNCT_1:11;
then A4: (canFS (f " {v})) . i in rng (canFS (f " {v})) by FUNCT_1:3;
f " {v} c= B ;
then A5: (canFS (f " {v})) . i in B by A4;
not (canFS (f " {v})) . i in Carrier l by A4, A3, XBOOLE_0:def 4;
then 0. F = l . ((canFS (f " {v})) . i) by A5
.= (Expand (f,l,v)) . i by A6, FUNCT_1:12 ;
hence (Expand (f,l,v)) . i = ((len (Expand (f,l,v))) |-> (0. F)) . i by A6, FINSEQ_2:57; :: thesis: verum

end;

then Expand (f,l,v) = (len (Expand (f,l,v))) |-> (0. F) by CARD_1:def 7;
then Sum (Expand (f,l,v)) = 0. F by MATRIX_3:11;
hence contradiction by B1, defK; :: thesis: verum

end;

then consider y being object such that
A8: y in f " {v} and
A9: y in Carrier l by XBOOLE_0:3;
A10: y in dom f by A8, FUNCT_1:def 7;
A11: f . y in {v} by A8, FUNCT_1:def 7;
reconsider y = y as Element of B by A8;
f . y = v by A11, TARSKI:def 1;
hence o in f .: (Carrier l) by B1, A9, A10, FUNCT_1:def 6; :: thesis: verum

end;

hence Carrier (f (#) l) c= f .: (Carrier l) ; :: thesis: verum