theorem Th34: :: FINSEQ_2:36

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