theorem Th8: :: FINSEQOP:8

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