let a be set ; :: thesis: 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
let p, r be FinSequence; :: thesis: for F being Function st [:(rng p),{a}:] c= dom F & r = F [:] p,a holds
len r = len p
let F be Function; :: thesis: ( [:(rng p),{a}:] c= dom F & r = F [:] p,a implies len r = len p )
assume [:(rng p),{a}:] c= dom F ; :: thesis: ( not r = F [:] p,a or len r = len p )
then dom (F [:] p,a) = dom p by Lm6;
then dom (F [:] p,a) = Seg (len p) by FINSEQ_1:def 3;
hence ( not r = F [:] p,a or len r = len p ) by FINSEQ_1:def 3; :: thesis: verum