let it1, it2 be FinSequence of OAlph; :: thesis: ( len it1 = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds
it1 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) & len it2 = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds
it2 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) implies it1 = it2 )
set qs9 = (qs,w) -admissible ;
assume that
A6: len it1 = (len w) + 1 and
A7: for i being Nat st i in Seg ((len w) + 1) holds
it1 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ; :: thesis: ( not len it2 = (len w) + 1 or ex i being Nat st
( i in Seg ((len w) + 1) & not it2 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) or it1 = it2 )
assume that
A8: len it2 = (len w) + 1 and
A9: for i being Nat st i in Seg ((len w) + 1) holds
it2 . i = the OFun of sfsm . (((qs,w) -admissible) . i) ; :: thesis: it1 = it2

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 A6, A8; :: 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 A10: i in Seg (len it1) by FINSEQ_1:1;
then it1 . i = the OFun of sfsm . (((qs,w) -admissible) . i) by A6, A7;
hence it1 . i = it2 . i by A6, A9, A10; :: thesis: verum

end;

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