for V being RealLinearSpace
for F being FinSequence of the carrier of V st F is one-to-one holds
for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L