theorem Th14: :: FINSEQOP:14

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