theorem XXX2: :: VECTSP13:7

for F being Field
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)