theorem :: FINSEQ_2:35

for x1 being object
for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1*> holds
f * p = <*(f . x1)*>