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 ;
A8: GEN (w2,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s2])*> by ;
A9: (GEN (w1,q)) . 3 = the Tran of S . [ the InitS of S,s1] by ;
A10: (GEN (w2,q)) . 3 = the Tran of S . [ the InitS of S,s2] by ;
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 ;
A16: (GEN ((w ^ w2), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s2] by ;
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 by FINSEQ_1:44;
A21: w2 . 1 = s by FINSEQ_1:44;
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
.= the Tran of S . [ the InitS of S,s1] by ;
(GEN (w2, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2] by
.= the Tran of S . [ the InitS of S,s2] by ;
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
.= s9 by FINSEQ_1:def 8 ;
A28: dom <*s9*> c= dom w by ;
then A29: (w ^ w1) . 1 = s9 by ;
A30: (w ^ w2) . 1 = s9 by ;
A31: (len (w ^ w1)) + 1 = ((len w) + 2) + 1 by ;
(len (w ^ w2)) + 1 = ((len w) + 2) + 1 by ;
hence contradiction by A2, A3, A15, A16, A29, A30, A31; :: thesis: verum
end;
end;