theorem Th25: :: LMODFREE:26

for D, E being non empty set
for h being Function of D,E
for p being FinSequence of D
for d being Element of D holds h * (p ^ <*d*>) = (h * p) ^ <*(h . d)*>