set qs' = qs,w -admissible ;
A1: Seg (len (qs,w -admissible )) = dom (qs,w -admissible ) by FINSEQ_1:def 3;
deffunc H₁( Nat) -> set = the OFun of sfsm . ((qs,w -admissible ) . $1);
consider p being FinSequence such that
A2: ( 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();
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 & 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 A1, A2, A3, FINSEQ_2:13;
p . x = the OFun of sfsm . qsx by A2, A3;
hence y in OAlph by A3; :: thesis: verum

end;

then reconsider p' = p as FinSequence of OAlph by FINSEQ_1:def 4;
A4: len (qs,w -admissible ) = (len w) + 1 by Def2;
dom p = dom (qs,w -admissible ) by A2, FINSEQ_3:31;
then ( len p' = len (qs,w -admissible ) & ( for i being Element of NAT st i in dom (qs,w -admissible ) holds
p' . i = the OFun of sfsm . ((qs,w -admissible ) . i) ) ) by A2;
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 A1, A4; :: thesis: verum