theorem Th5: :: MATRIX15:5

for f being Function
for p1, p2, f1, f2 being FinSequence st rng p1 c= dom f & rng p2 c= dom f & f1 = f * p1 & f2 = f * p2 holds
f * (p1 ^ p2) = f1 ^ f2