let qs1, qs2 be FinSequence of the carrier of fsm; :: thesis: ( qs1 . 1 = q & len qs1 = (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 = qs1 . i & qi1 = qs1 . (i + 1) & wi -succ_of qi = qi1 ) ) & qs2 . 1 = q & len qs2 = (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 = qs2 . i & qi1 = qs2 . (i + 1) & wi -succ_of qi = qi1 ) ) implies qs1 = qs2 )
assume that
A5: qs1 . 1 = q and
A6: len qs1 = (len w) + 1 and
A7: for i being Nat st 1 <= i & i <= len w holds
ex wi being Element of IAlph ex qs1i, qs1i1 being State of fsm st
( wi = w . i & qs1i = qs1 . i & qs1i1 = qs1 . (i + 1) & wi -succ_of qs1i = qs1i1 ) and
A8: qs2 . 1 = q and
A9: len qs2 = (len w) + 1 and
A10: for i being Nat st 1 <= i & i <= len w holds
ex wi being Element of IAlph ex qs2i, qs2i1 being State of fsm st
( wi = w . i & qs2i = qs2 . i & qs2i1 = qs2 . (i + 1) & wi -succ_of qs2i = qs2i1 ) ; :: thesis: qs1 = qs2
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len qs1 implies qs1 . $1 = qs2 . $1 );

A11: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume that
1 <= k + 1 and
A13: k + 1 <= len qs1 ; :: thesis: qs1 . (k + 1) = qs2 . (k + 1)
A14: ( 0 = k or ( 0 < k & 0 + 1 = 1 ) ) ;

per cases ( 0 = k or 1 <= k ) by A14, NAT_1:13;

suppose 0 = k ; :: thesis: qs1 . (k + 1) = qs2 . (k + 1)

hence qs1 . (k + 1) = qs2 . (k + 1) by A5, A8; :: thesis: verum

end;

suppose A15: 1 <= k ; :: thesis: qs1 . (k + 1) = qs2 . (k + 1)

A16: k <= len w by A6, A13, XREAL_1:6;
then ( ex i1 being Element of IAlph ex qs1i, qs1i1 being State of fsm st
( i1 = w . k & qs1i = qs1 . k & qs1i1 = qs1 . (k + 1) & i1 -succ_of qs1i = qs1i1 ) & ex i2 being Element of IAlph ex qs2i, qs2i1 being State of fsm st
( i2 = w . k & qs2i = qs2 . k & qs2i1 = qs2 . (k + 1) & i2 -succ_of qs2i = qs2i1 ) ) by A7, A10, A15;
hence qs1 . (k + 1) = qs2 . (k + 1) by A6, A12, A15, A16, NAT_1:12; :: thesis: verum

end;

end;

end;

end;

A17: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A17, A11);
hence qs1 = qs2 by A6, A9, FINSEQ_1:14; :: thesis: verum