theorem Th65: :: FINSEQ_2:67

for a being object
for p, r being FinSequence
for F being Function st [:{a},(rng p):] c= dom F & r = F [;] (a,p) holds
len r = len p