let I be non empty set ; :: thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds
for s, s1, s2 being Element of I
for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S
let S be non empty FSM over I; :: thesis: ( S is regular & S is calculating_type implies for s, s1, s2 being Element of I
for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S )
assume that
A1: S is regular and
A2: S is calculating_type ; :: thesis: for s, s1, s2 being Element of I
for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S
let s, s1, s2 be Element of I; :: thesis: for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S
let q be State of S; :: thesis: ( the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] implies the Tran of S . [q,s] <> the InitS of S )
assume A3: the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] ; :: thesis: the Tran of S . [q,s] <> the InitS of S
q is accessible by A1;
then consider w being FinSequence of I such that
A4: the InitS of S,w -leads_to q ;
A5: (GEN (w, the InitS of S)) . ((len w) + 1) = q by A4;
assume A6: the Tran of S . [q,s] = the InitS of S ; :: thesis: contradiction
reconsider w1 = <*s,s1*>, w2 = <*s,s2*> as FinSequence of I ;
A7: GEN (w1,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s1])*> by A6, Th2;
A8: GEN (w2,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s2])*> by A6, Th2;
A9: (GEN (w1,q)) . 3 = the Tran of S . [ the InitS of S,s1] by A7;
A10: (GEN (w2,q)) . 3 = the Tran of S . [ the InitS of S,s2] by A8;
A11: len w1 = 2 by FINSEQ_1:44;
A12: len w2 = 2 by FINSEQ_1:44;
A13: 3 <= (len w1) + 1 by A11;
A14: 3 <= (len w2) + 1 by A12;
A15: (GEN ((w ^ w1), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s1] by A4, A9, A13, FSM_1:7;
A16: (GEN ((w ^ w2), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s2] by A4, A10, A14, FSM_1:7;

per cases ( w = {} or w <> {} ) ;

suppose w = {} ; :: thesis: contradiction

then A17: len w = 0 ;
A18: GEN (w1, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1])*> by Th2;
A19: GEN (w2, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2])*> by Th2;
A20: w1 . 1 = s ;
A21: w2 . 1 = s ;
A22: 3 <= (len w1) + 1 by A11;
A23: 3 <= (len w2) + 1 by A12;
A24: (GEN (w1, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1] by A18
.= the Tran of S . [ the InitS of S,s1] by A5, A6, A17, FSM_1:def 2 ;
(GEN (w2, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2] by A19
.= the Tran of S . [ the InitS of S,s2] by A5, A6, A17, FSM_1:def 2 ;
hence contradiction by A2, A3, A20, A21, A22, A23, A24; :: thesis: verum

end;

suppose w <> {} ; :: thesis: contradiction

then consider s9 being object , w9 being FinSequence such that
A25: w = <*s9*> ^ w9 and
len w = (len w9) + 1 by REWRITE1:5;
dom <*s9*> = Seg 1 by FINSEQ_1:def 8;
then A26: 1 in dom <*s9*> by FINSEQ_1:1;
then A27: w . 1 = <*s9*> . 1 by A25, FINSEQ_1:def 7
.= s9 ;
A28: dom <*s9*> c= dom w by A25, FINSEQ_1:26;
then A29: (w ^ w1) . 1 = s9 by A26, A27, FINSEQ_1:def 7;
A30: (w ^ w2) . 1 = s9 by A26, A27, A28, FINSEQ_1:def 7;
A31: (len (w ^ w1)) + 1 = ((len w) + 2) + 1 by A11, FINSEQ_1:22;
(len (w ^ w2)) + 1 = ((len w) + 2) + 1 by A12, FINSEQ_1:22;
hence contradiction by A2, A3, A15, A16, A29, A30, A31; :: thesis: verum

end;

end;