theorem Th87: :: MATRIX13:87

for K being Field
for a being Element of K
for p, pf being FinSequence of K
for f being Function st pf = p * f & rng f c= dom p holds
(a * p) * f = a * pf