theorem Th64: :: FINSEQ_2:66

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