theorem :: FINSEQ_2:87

for D, D9, E being non empty set
for d1, d2 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*> holds
F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9))*>