let I be non empty set ; :: thesis: for s being Element of I
for S being non empty FSM over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non zero Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )

let s be Element of I; :: thesis: for S being non empty FSM over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non zero Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )

let S be non empty FSM over I; :: thesis: for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non zero Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )

let q be State of S; :: thesis: ( S is calculating_type & q is_accessible_via s implies ex m being non zero Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) ) )

assume A1: S is calculating_type ; :: thesis: ( not q is_accessible_via s or ex m being non zero Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) ) )

given w being FinSequence of I such that A2: the InitS of S,<*s*> ^ w -leads_to q ; :: according to FSM_2:def 2 :: thesis: ex m being non zero Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )

defpred S1[ Nat] means ( q = (GEN ((<*s*> ^ w), the InitS of S)) . \$1 & \$1 >= 1 & \$1 <= (len (<*s*> ^ w)) + 1 );
A3: (len (<*s*> ^ w)) + 1 >= 1 by NAT_1:11;
q = (GEN ((<*s*> ^ w), the InitS of S)) . ((len (<*s*> ^ w)) + 1) by A2;
then A4: ex m being Nat st S1[m] by A3;
consider m being Nat such that
A5: S1[m] and
A6: for k being Nat st S1[k] holds
m <= k from reconsider m = m as non zero Element of NAT by ;
take m ; :: thesis: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN (w, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )

let w1 be FinSequence of I; :: thesis: ( (len w1) + 1 >= m & w1 . 1 = s implies ( q = (GEN (w1, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q ) ) )

assume that
A7: (len w1) + 1 >= m and
A8: w1 . 1 = s ; :: thesis: ( q = (GEN (w1, the InitS of S)) . m & ( for i being non zero Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q ) )

(<*s*> ^ w) . 1 = s by FINSEQ_1:41;
then GEN (w1, the InitS of S), GEN ((<*s*> ^ w), the InitS of S) are_c=-comparable by A1, A8, Th4;
then A9: ( GEN (w1, the InitS of S) c= GEN ((<*s*> ^ w), the InitS of S) or GEN ((<*s*> ^ w), the InitS of S) c= GEN (w1, the InitS of S) ) ;
A10: dom (GEN ((<*s*> ^ w), the InitS of S)) = Seg (len (GEN ((<*s*> ^ w), the InitS of S))) by FINSEQ_1:def 3
.= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def 2 ;
A11: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def 3
.= Seg ((len w1) + 1) by FSM_1:def 2 ;
A12: m in dom (GEN ((<*s*> ^ w), the InitS of S)) by ;
m in dom (GEN (w1, the InitS of S)) by ;
hence q = (GEN (w1, the InitS of S)) . m by ; :: thesis: for i being non zero Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q

let i be non zero Element of NAT ; :: thesis: ( i < m implies (GEN (w1, the InitS of S)) . i <> q )
assume A13: i < m ; :: thesis: (GEN (w1, the InitS of S)) . i <> q
A14: 1 <= i by NAT_1:14;
A15: i <= (len (<*s*> ^ w)) + 1 by ;
A16: i <= (len w1) + 1 by ;
A17: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def 3
.= Seg ((len w1) + 1) by FSM_1:def 2 ;
dom (GEN ((<*s*> ^ w), the InitS of S)) = Seg (len (GEN ((<*s*> ^ w), the InitS of S))) by FINSEQ_1:def 3
.= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def 2 ;
then A18: i in dom (GEN ((<*s*> ^ w), the InitS of S)) by ;
A19: i in dom (GEN (w1, the InitS of S)) by ;
assume (GEN (w1, the InitS of S)) . i = q ; :: thesis: contradiction
then q = (GEN ((<*s*> ^ w), the InitS of S)) . i by ;
hence contradiction by A6, A13, A14, A15; :: thesis: verum