theorem Th38: :: RANKNULL:38
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @ l) (#) (T * G)