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

now :: thesis: for v being Element of V holds (f (#) (l (#) f)) . v = l . v

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

per cases ( v in rng f or not v in rng f ) ;

suppose C: v in rng f ; :: thesis: (f (#) (l (#) f)) . b₁ = l . b₁

then consider u being object such that
D: ( u in dom f & f . u = v ) by FUNCT_1:def 3;
reconsider u = u as Element of U by H, D;
E: (f ") . v = u by D, A, FUNCT_1:34;
(l (#) f) . u = l . (f . u) by D, defK1;
hence (f (#) (l (#) f)) . v = l . v by D, E, C, A, XXX2; :: thesis: verum

end;

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

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

end;

end;

end;

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