theorem :: FINSEQ_2:88

for D, D9, E being non empty set
for d1, d2, d3 being Element of D
for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D st p = <*d1,d2,d3*> holds
F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*>