set qs9 = (qs,w) -admissible ;
deffunc H₁( Nat) -> set = the OFun of sfsm . (((qs,w) -admissible) . $1);
consider p being FinSequence such that
A1: ( len p = len ((qs,w) -admissible) & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A2: Seg (len ((qs,w) -admissible)) = dom ((qs,w) -admissible) by FINSEQ_1:def 3;
rng p c= OAlph

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in OAlph )
assume y in rng p ; :: thesis: y in OAlph
then consider x being object such that
A3: x in dom p and
A4: y = p . x by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
dom p = Seg (len p) by FINSEQ_1:def 3;
then reconsider qsx = ((qs,w) -admissible) . x as State of sfsm by A2, A1, A3, FINSEQ_2:11;
p . x = the OFun of sfsm . qsx by A1, A3;
hence y in OAlph by A4; :: thesis: verum

end;

then reconsider p9 = p as FinSequence of OAlph by FINSEQ_1:def 4;
A5: len ((qs,w) -admissible) = (len w) + 1 by Def2;
dom p = dom ((qs,w) -admissible) by A1, FINSEQ_3:29;
then for i being Nat st i in dom ((qs,w) -admissible) holds
p9 . i = the OFun of sfsm . (((qs,w) -admissible) . i) by A1;
hence ex b₁ being FinSequence of OAlph st
( len b₁ = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds
b₁ . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) ) by A2, A1, A5; :: thesis: verum