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 st f is one-to-one holds
for l being Linear_Combination of B
for v being Element of V st v in rng f holds
(f (#) l) . v = l . ((f ") . v)
let U, V be VectSp of F; :: thesis: for B being non empty finite Subset of U
for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of B
for v being Element of V st v in rng f holds
(f (#) l) . v = l . ((f ") . v)
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V st f is one-to-one holds
for l being Linear_Combination of B
for v being Element of V st v in rng f holds
(f (#) l) . v = l . ((f ") . v)
let f be Function of B,V; :: thesis: ( f is one-to-one implies for l being Linear_Combination of B
for v being Element of V st v in rng f holds
(f (#) l) . v = l . ((f ") . v) )
assume A: f is one-to-one ; :: thesis: for l being Linear_Combination of B
for v being Element of V st v in rng f holds
(f (#) l) . v = l . ((f ") . v)
let l be Linear_Combination of B; :: thesis: for v being Element of V st v in rng f holds
(f (#) l) . v = l . ((f ") . v)
let v be Element of V; :: thesis: ( v in rng f implies (f (#) l) . v = l . ((f ") . v) )
assume B: v in rng f ; :: thesis: (f (#) l) . v = l . ((f ") . v)
then consider x being object such that
C: ( x in dom f & f . x = v ) by FUNCT_1:def 3;
I: dom f = B by FUNCT_2:def 1;
then reconsider u = x as Element of U by C;
H: dom l = the carrier of U by FUNCT_2:def 1;
v in dom (f ") by A, B, FUNCT_1:33;
then (f ") . v in rng (f ") by FUNCT_1:3;
then K: (f ") . v in dom f by A, FUNCT_1:33;
then J: (f ") . v in U by I;
D: l . ((f ") . v) in rng l by K, I, H, FUNCT_1:3;
G: f " {v} = {((f ") . v)} by A, B, XXX1;
then E: canFS (f " {v}) = <*((f ") . v)*> by FINSEQ_1:94;
set G = l * (canFS (f " {v}));
F: dom (l * (canFS (f " {v}))) = Seg 1

proof

F1: now :: thesis: for o being object st o in Seg 1 holds
o in dom (l * (canFS (f " {v})))

let o be object ; :: thesis: ( o in Seg 1 implies o in dom (l * (canFS (f " {v}))) )
assume o in Seg 1 ; :: thesis: o in dom (l * (canFS (f " {v})))
then F2: o in dom (canFS (f " {v})) by E, FINSEQ_1:38;
then (canFS (f " {v})) . o in rng (canFS (f " {v})) by FUNCT_1:3;
then (canFS (f " {v})) . o = (f ") . v by G, TARSKI:def 1;
then (canFS (f " {v})) . o in dom l by J, FUNCT_2:def 1;
hence o in dom (l * (canFS (f " {v}))) by F2, FUNCT_1:11; :: thesis: verum

end;

now :: thesis: for o being object st o in dom (l * (canFS (f " {v}))) holds
o in Seg 1

let o be object ; :: thesis: ( o in dom (l * (canFS (f " {v}))) implies o in Seg 1 )
assume o in dom (l * (canFS (f " {v}))) ; :: thesis: o in Seg 1
then o in dom (canFS (f " {v})) by FUNCT_1:11;
hence o in Seg 1 by E, FINSEQ_1:38; :: thesis: verum

end;

hence dom (l * (canFS (f " {v}))) = Seg 1 by F1, TARSKI:2; :: thesis: verum

end;

then reconsider G = l * (canFS (f " {v})) as FinSequence by FINSEQ_1:def 2;

now :: thesis: for o being object st o in rng G holds
o in the carrier of F

let o be object ; :: thesis: ( o in rng G implies o in the carrier of F )
assume o in rng G ; :: thesis: o in the carrier of F
then o in rng l by FUNCT_1:14;
hence o in the carrier of F ; :: thesis: verum

end;

then rng G c= the carrier of F ;
then reconsider G = G as FinSequence of the carrier of F by FINSEQ_1:def 4;
dom (canFS (f " {v})) = Seg 1 by E, FINSEQ_1:38;
then 1 in dom (canFS (f " {v})) ;
then G . 1 = l . ((canFS (f " {v})) . 1) by FUNCT_1:13
.= l . ((f ") . v) by E ;
then l * (canFS (f " {v})) = <*(l . ((f ") . v))*> by F, FINSEQ_1:def 8;
then Sum (Expand (f,l,v)) = l . ((f ") . v) by D, RLVECT_1:44;
hence (f (#) l) . v = l . ((f ") . v) by defK; :: thesis: verum