theorem CLS: :: VECTSP13:17

for F being Field
for U being non trivial finite-dimensional VectSp of F
for V being VectSp of F
for B being Basis of U
for f being Function of B,V
for l being Linear_Combination of B holds (canLinTrans f) . (Sum l) = Sum (f (#) l)