theorem Th63: :: FINSEQ_2:65

for p, q, r being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F & r = F .: (p,q) holds
len r = min ((len p),(len q))