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 set ; :: 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 set such that
A3: x in dom p and
A4: y = p . x by FUNCT_1:def 5;
reconsider x = x as Element of 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:13;
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:31;
then for i being Element of 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 Element of 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