theorem Th67: :: FINSEQ_2:69

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