theorem ThTF3B2: :: ZMODUL05:45

for V, W being Z_Module
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