theorem :: FINSEQ_2:74

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