theorem Th82: :: FINSEQ_2:84

for D, D9, E being non empty set
for d9 being Element of D9
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D st r = F [:] (p,d9) holds
len r = len p