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 s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

let S be non empty FSM over I; :: thesis: ( S is regular & S is calculating_type implies for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] )

assume that

A1: S is regular and

A2: S is calculating_type ; :: thesis: for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

let s1, s2 be Element of I; :: thesis: for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

let q be State of S; :: thesis: ( q <> the InitS of S implies the Tran of S . [q,s1] = the Tran of S . [q,s2] )

assume A3: q <> the InitS of S ; :: thesis: the Tran of S . [q,s1] = the Tran of S . [q,s2]

set w1 = <*s1*>;

set w2 = <*s2*>;

A4: len <*s1*> = 0 + 1 by FINSEQ_1:39;

reconsider j = len <*s1*> as non zero Element of NAT ;

consider WI being Element of I, QI, QI1 being State of S such that

A5: WI = <*s1*> . j and

A6: QI = (GEN (<*s1*>,q)) . j and

A7: QI1 = (GEN (<*s1*>,q)) . (j + 1) and

A8: WI -succ_of QI = QI1 by A4, FSM_1:def 2;

WI = s1 by A4, A5, FINSEQ_1:def 8;

then A9: QI1 = s1 -succ_of q by A4, A6, A8, FSM_1:def 2;

A10: len <*s2*> = 0 + 1 by FINSEQ_1:39;

reconsider h = len <*s2*> as non zero Element of NAT ;

consider WI2 being Element of I, QI2, QI12 being State of S such that

A11: WI2 = <*s2*> . h and

A12: QI2 = (GEN (<*s2*>,q)) . h and

A13: QI12 = (GEN (<*s2*>,q)) . (h + 1) and

A14: WI2 -succ_of QI2 = QI12 by A10, FSM_1:def 2;

A15: QI2 = q by A10, A12, FSM_1:def 2;

WI2 = s2 by A10, A11, FINSEQ_1:def 8;

hence the Tran of S . [q,s1] = the Tran of S . [q,s2] by A1, A2, A3, A4, A7, A9, A10, A13, A14, A15, Th14; :: thesis: verum

for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

let S be non empty FSM over I; :: thesis: ( S is regular & S is calculating_type implies for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] )

assume that

A1: S is regular and

A2: S is calculating_type ; :: thesis: for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

let s1, s2 be Element of I; :: thesis: for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2]

let q be State of S; :: thesis: ( q <> the InitS of S implies the Tran of S . [q,s1] = the Tran of S . [q,s2] )

assume A3: q <> the InitS of S ; :: thesis: the Tran of S . [q,s1] = the Tran of S . [q,s2]

set w1 = <*s1*>;

set w2 = <*s2*>;

A4: len <*s1*> = 0 + 1 by FINSEQ_1:39;

reconsider j = len <*s1*> as non zero Element of NAT ;

consider WI being Element of I, QI, QI1 being State of S such that

A5: WI = <*s1*> . j and

A6: QI = (GEN (<*s1*>,q)) . j and

A7: QI1 = (GEN (<*s1*>,q)) . (j + 1) and

A8: WI -succ_of QI = QI1 by A4, FSM_1:def 2;

WI = s1 by A4, A5, FINSEQ_1:def 8;

then A9: QI1 = s1 -succ_of q by A4, A6, A8, FSM_1:def 2;

A10: len <*s2*> = 0 + 1 by FINSEQ_1:39;

reconsider h = len <*s2*> as non zero Element of NAT ;

consider WI2 being Element of I, QI2, QI12 being State of S such that

A11: WI2 = <*s2*> . h and

A12: QI2 = (GEN (<*s2*>,q)) . h and

A13: QI12 = (GEN (<*s2*>,q)) . (h + 1) and

A14: WI2 -succ_of QI2 = QI12 by A10, FSM_1:def 2;

A15: QI2 = q by A10, A12, FSM_1:def 2;

WI2 = s2 by A10, A11, FINSEQ_1:def 8;

hence the Tran of S . [q,s1] = the Tran of S . [q,s2] by A1, A2, A3, A4, A7, A9, A10, A13, A14, A15, Th14; :: thesis: verum