theorem :: VECTSP12:1

for K being Field
for V, W being finite-dimensional VectSp of K
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W
for l being Linear_Combination of B \ A st A is Basis of (ker T) & A c= B holds
T . (Sum l) = Sum (T @* l)