let I be non empty set ; :: thesis: for S being non empty FSM of 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 of 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 A1: ( S is regular & 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 A2: q <> the InitS of S ; :: thesis: the Tran of S . [q,s1] = the Tran of S . [q,s2]
set w1 = <*s1*>;
set w2 = <*s2*>;
A3: len <*s1*> = 0 + 1 by FINSEQ_1:56;
reconsider j = len <*s1*> as non empty Element of NAT ;
consider WI being Element of I, QI, QI1 being State of S such that
A4: ( WI = <*s1*> . j & QI = (GEN <*s1*>,q) . j & QI1 = (GEN <*s1*>,q) . (j + 1) & WI -succ_of QI = QI1 ) by A3, FSM_1:def 2;
WI = s1 by A3, A4, FINSEQ_1:def 8;
then A5: QI1 = s1 -succ_of q by A3, A4, FSM_1:def 2;
A6: len <*s2*> = 0 + 1 by FINSEQ_1:56;
reconsider h = len <*s2*> as non empty Element of NAT ;
consider WI2 being Element of I, QI2, QI12 being State of S such that
A7: ( WI2 = <*s2*> . h & QI2 = (GEN <*s2*>,q) . h & QI12 = (GEN <*s2*>,q) . (h + 1) & WI2 -succ_of QI2 = QI12 ) by A6, FSM_1:def 2;
A8: QI2 = q by A6, A7, FSM_1:def 2;
WI2 = s2 by A6, A7, FINSEQ_1:def 8;
hence the Tran of S . [q,s1] = the Tran of S . [q,s2] by A1, A2, A3, A4, A5, A6, A7, A8, Th14; :: thesis: verum