let a be object ; :: thesis: for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
F [:] (p,a) is FinSequence
let p be FinSequence; :: thesis: for F being Function st [:(rng p),{a}:] c= dom F holds
F [:] (p,a) is FinSequence
let F be Function; :: thesis: ( [:(rng p),{a}:] c= dom F implies F [:] (p,a) is FinSequence )
assume [:(rng p),{a}:] c= dom F ; :: thesis: F [:] (p,a) is FinSequence
then dom (F [:] (p,a)) = dom p by Lm5;
then dom (F [:] (p,a)) = Seg (len p) by FINSEQ_1:def 3;
hence F [:] (p,a) is FinSequence by FINSEQ_1:def 2; :: thesis: verum