theorem Th88: :: MATRIX13:88

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