let it1, it2 be FinSequence of OAlph; ( len it1 = len w & ( for i being Nat st i in dom w holds
it1 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) & len it2 = len w & ( for i being Nat st i in dom w holds
it2 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) implies it1 = it2 )
set qs = (qt,w) -admissible ;
assume that
A7:
len it1 = len w
and
A8:
for i being Nat st i in dom w holds
it1 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)]
; ( not len it2 = len w or ex i being Nat st
( i in dom w & not it2 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) or it1 = it2 )
assume that
A9:
len it2 = len w
and
A10:
for i being Nat st i in dom w holds
it2 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)]
; it1 = it2
A11:
dom w = dom it1
by A7, FINSEQ_3:29;
hence
it1 = it2
by FINSEQ_1:14; verum