for K being Field
for V, W being VectSp of K
for T being linear-transformation of V,W
for A being Subset of V
for L being Linear_Combination of A st T | A is one-to-one holds
T . (Sum L) = Sum (T @ L)