theorem Th35: :: FINSEQ_2:37

for x1, x2, x3 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,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>