set N = (len w) + 1;
set D = the carrier of fsm;
defpred S₁[ Nat, set , set ] means ex wn being Element of IAlph ex q9, q99 being Element of the carrier of fsm st
( w . $1 = wn & q9 = $2 & q99 = $3 & wn -succ_of q9 = q99 );
A1: for n being Nat st 1 <= n & n < (len w) + 1 holds
for x being Element of the carrier of fsm ex y being Element of the carrier of fsm st S₁[n,x,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < (len w) + 1 implies for x being Element of the carrier of fsm ex y being Element of the carrier of fsm st S₁[n,x,y] )
assume A2: 1 <= n ; :: thesis: ( not n < (len w) + 1 or for x being Element of the carrier of fsm ex y being Element of the carrier of fsm st S₁[n,x,y] )
assume n < (len w) + 1 ; :: thesis: for x being Element of the carrier of fsm ex y being Element of the carrier of fsm st S₁[n,x,y]
then n <= len w by NAT_1:13;
then n in dom w by A2, FINSEQ_3:25;
then reconsider wn = w . n as Element of IAlph by FINSEQ_2:11;
let x be Element of the carrier of fsm; :: thesis: ex y being Element of the carrier of fsm st S₁[n,x,y]
wn -succ_of x = the Tran of fsm . [x,wn] ;
hence ex y being Element of the carrier of fsm st S₁[n,x,y] ; :: thesis: verum

end;

consider p being FinSequence of the carrier of fsm such that
A3: ( len p = (len w) + 1 & ( p . 1 = q or (len w) + 1 = 0 ) & ( for n being Nat st 1 <= n & n < (len w) + 1 holds
S₁[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch 4(A1);
take p ; :: thesis: ( p . 1 = q & len p = (len w) + 1 & ( for i being Nat st 1 <= i & i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = p . i & qi1 = p . (i + 1) & wi -succ_of qi = qi1 ) ) )
thus p . 1 = q by A3; :: thesis: ( len p = (len w) + 1 & ( for i being Nat st 1 <= i & i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = p . i & qi1 = p . (i + 1) & wi -succ_of qi = qi1 ) ) )
thus len p = (len w) + 1 by A3; :: thesis: for i being Nat st 1 <= i & i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = p . i & qi1 = p . (i + 1) & wi -succ_of qi = qi1 )
let i be Nat; :: thesis: ( 1 <= i & i <= len w implies ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = p . i & qi1 = p . (i + 1) & wi -succ_of qi = qi1 ) )
assume A4: 1 <= i ; :: thesis: ( not i <= len w or ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = p . i & qi1 = p . (i + 1) & wi -succ_of qi = qi1 ) )
assume i <= len w ; :: thesis: ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = p . i & qi1 = p . (i + 1) & wi -succ_of qi = qi1 )
then ( i in NAT & i < (len w) + 1 ) by NAT_1:13, ORDINAL1:def 12;
hence ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = p . i & qi1 = p . (i + 1) & wi -succ_of qi = qi1 ) by A3, A4; :: thesis: verum