theorem ThTF3B2: :: ZMODUL05:45

for K being Ring
for V, W being LeftMod of K
for T being linear-transformation of V,W
for s being Vector of W
for A being Subset of V
for l being Linear_Combination of A st ( for v being Vector of V st v in Carrier l holds
T . v = s ) holds
T . (Sum l) = (Sum (lCFST (l,T,s))) * s