set qs = (qt,w) -admissible ;
deffunc H1( Nat) -> set = the OFun of tfsm . [(((qt,w) -admissible) . $1),(w . $1)];
consider p being FinSequence such that
A1:
( len p = len w & ( for i being Nat st i in dom p holds
p . i = H1(i) ) )
from FINSEQ_1:sch 2();
A2:
Seg (len w) = dom w
by FINSEQ_1:def 3;
rng p c= OAlph
proof
let y be
object ;
TARSKI:def 3 ( not y in rng p or y in OAlph )
assume
y in rng p
;
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;
x <= len p
by A3, FINSEQ_3:25;
then A5:
x <= (len p) + 1
by NAT_1:12;
A6:
len ((qt,w) -admissible) = (len p) + 1
by A1, Def2;
dom p = Seg (len p)
by FINSEQ_1:def 3;
then reconsider wx =
w . x as
Element of
IAlph by A2, A1, A3, FINSEQ_2:11;
1
<= x
by A3, FINSEQ_3:25;
then
x in dom ((qt,w) -admissible)
by A6, A5, FINSEQ_3:25;
then reconsider qsx =
((qt,w) -admissible) . x as
Element of
tfsm by FINSEQ_2:11;
p . x = the
OFun of
tfsm . [qsx,wx]
by A1, A3;
hence
y in OAlph
by A4;
verum
end;
then reconsider p9 = p as FinSequence of OAlph by FINSEQ_1:def 4;
dom p = dom w
by A1, FINSEQ_3:29;
then
for i being Nat st i in dom w holds
p9 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)]
by A1;
hence
ex b1 being FinSequence of OAlph st
( len b1 = len w & ( for i being Nat st i in dom w holds
b1 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) )
by A1; verum