theorem Th70: :: FINSEQ_2:72

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