theorem Th66: :: FINSEQ_2:68

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