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