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 holds (f (#) l) (#) f = 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 st f is one-to-one holds
for l being Linear_Combination of B holds (f (#) l) (#) f = l
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 holds (f (#) l) (#) f = l
let f be Function of B,V; :: thesis: ( f is one-to-one implies for l being Linear_Combination of B holds (f (#) l) (#) f = l )
assume A: f is one-to-one ; :: thesis: for l being Linear_Combination of B holds (f (#) l) (#) f = l
let l be Linear_Combination of B; :: thesis: (f (#) l) (#) f = l
set l2 = f (#) l;
H: dom f = B by FUNCT_2:def 1;

now :: thesis: for u being Element of U holds ((f (#) l) (#) f) . u = l . u

let u be Element of U; :: thesis: ((f (#) l) (#) f) . b₁ = l . b₁

per cases ( u in B or not u in B ) ;

suppose C: u in B ; :: thesis: ((f (#) l) (#) f) . b₁ = l . b₁

then f . u in rng f by H, FUNCT_1:3;
then reconsider v = f . u as Element of V ;
(f (#) l) . v = l . ((f ") . v) by A, C, H, FUNCT_1:3, XXX2;
hence ((f (#) l) (#) f) . u = l . ((f ") . v) by C, defK1
.= l . u by A, C, H, FUNCT_1:34 ;
:: thesis: verum

end;

suppose C: not u in B ; :: thesis: ((f (#) l) (#) f) . b₁ = l . b₁

Carrier l c= B by VECTSP_6:def 4;
then not u in Carrier l by C;
then D: l . u = 0. F ;
Carrier ((f (#) l) (#) f) c= B by VECTSP_6:def 4;
then not u in Carrier ((f (#) l) (#) f) by C;
hence ((f (#) l) (#) f) . u = l . u by D; :: thesis: verum

end;

end;

end;

hence (f (#) l) (#) f = l by VECTSP_6:def 7; :: thesis: verum