let it1, it2 be FinSequence of OAlph; :: thesis: ( 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)] ; :: thesis: ( 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)] ; :: thesis: it1 = it2
A11: dom w = dom it1 by A7, FINSEQ_3:29;

now :: thesis: ( len it1 = len it2 & ( for i being Nat st 1 <= i & i <= len it1 holds
it1 . i = it2 . i ) )

thus len it1 = len it2 by A7, A9; :: thesis: for i being Nat st 1 <= i & i <= len it1 holds
it1 . i = it2 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len it1 implies it1 . i = it2 . i )
assume ( 1 <= i & i <= len it1 ) ; :: thesis: it1 . i = it2 . i
then A12: i in dom it1 by FINSEQ_3:25;
then it1 . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] by A8, A11;
hence it1 . i = it2 . i by A10, A11, A12; :: thesis: verum

end;

hence it1 = it2 by FINSEQ_1:14; :: thesis: verum