for K being Ring
for V, W being LeftMod of K
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for Tl being Linear_Combination of T .: (Carrier l) st Tl = T @* l holds
T . (Sum l) = Sum Tl