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
(GEN <*s1*>,q) . 2 = (GEN <*s2*>,q) . 2
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
(GEN <*s1*>,q) . 2 = (GEN <*s2*>,q) . 2 )
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
(GEN <*s1*>,q) . 2 = (GEN <*s2*>,q) . 2
let s1, s2 be Element of I; :: thesis: for q being State of S st q <> the InitS of S holds
(GEN <*s1*>,q) . 2 = (GEN <*s2*>,q) . 2
let q be State of S; :: thesis: ( q <> the InitS of S implies (GEN <*s1*>,q) . 2 = (GEN <*s2*>,q) . 2 )
assume A2: q <> the InitS of S ; :: thesis: (GEN <*s1*>,q) . 2 = (GEN <*s2*>,q) . 2
q is accessible by A1, Def4;
then consider w being FinSequence of I such that
A3: the InitS of S,w -leads_to q by Def3;
w <> {}

proof

assume w = {} ; :: thesis: contradiction
then len w = 0 ;
then (GEN w,the InitS of S) . ((len w) + 1) = the InitS of S by FSM_1:def 2;
hence contradiction by A2, A3, FSM_1:def 3; :: thesis: verum

end;

then consider x being Element of I, w' being FinSequence of I such that
A4: ( w . 1 = x & w = <*x*> ^ w' ) by FINSEQ_3:111;
set w1 = w ^ <*s1*>;
set w2 = w ^ <*s2*>;
len <*x*> = 1 by FINSEQ_1:56;
then (len <*x*>) + (len w') >= 1 by NAT_1:11;
then len w >= 1 by A4, FINSEQ_1:35;
then A5: 1 in dom w by FINSEQ_3:27;
then w . 1 = (w ^ <*s1*>) . 1 by FINSEQ_1:def 7;
then A6: (w ^ <*s1*>) . 1 = (w ^ <*s2*>) . 1 by A5, FINSEQ_1:def 7;
A7: len <*s1*> = 1 by FINSEQ_1:56;
then A8: len (w ^ <*s1*>) = (len w) + 1 by FINSEQ_1:35;
A9: len <*s2*> = 1 by FINSEQ_1:56;
then A10: len (w ^ <*s2*>) = (len w) + 1 by FINSEQ_1:35;
A11: len (w ^ <*s1*>) = len (w ^ <*s2*>) by A8, A9, FINSEQ_1:35;
set p = Del (GEN w,the InitS of S),((len w) + 1);
set p1 = GEN <*s1*>,q;
A12: GEN (w ^ <*s1*>),the InitS of S = (Del (GEN w,the InitS of S),((len w) + 1)) ^ (GEN <*s1*>,q) by A3, FSM_1:23;
A13: len (GEN w,the InitS of S) = (len w) + 1 by FSM_1:def 2;
then A14: len (Del (GEN w,the InitS of S),((len w) + 1)) = len w by MATRLIN:3;
A15: len (GEN <*s1*>,q) = (len <*s1*>) + 1 by FSM_1:def 2
.= 1 + 1 by FINSEQ_1:56 ;
A16: len (GEN (w ^ <*s1*>),the InitS of S) = len ((Del (GEN w,the InitS of S),((len w) + 1)) ^ (GEN <*s1*>,q)) by A3, FSM_1:23
.= (len (Del (GEN w,the InitS of S),((len w) + 1))) + (len (GEN <*s1*>,q)) by FINSEQ_1:35
.= (len w) + (1 + 1) by A13, A15, MATRLIN:3
.= ((len w) + 1) + 1
.= (len (w ^ <*s1*>)) + 1 by A7, FINSEQ_1:35 ;
A17: (len (Del (GEN w,the InitS of S),((len w) + 1))) + 1 <= (len (w ^ <*s1*>)) + 1 by A8, A14, NAT_1:11;
len ((Del (GEN w,the InitS of S),((len w) + 1)) ^ (GEN <*s1*>,q)) = (len (w ^ <*s1*>)) + 1 by A3, A16, FSM_1:23;
then (len (Del (GEN w,the InitS of S),((len w) + 1))) + (len (GEN <*s1*>,q)) = (len (w ^ <*s1*>)) + 1 by FINSEQ_1:35;
then A18: (GEN (w ^ <*s1*>),the InitS of S) . ((len (w ^ <*s1*>)) + 1) = (GEN <*s1*>,q) . (((len (w ^ <*s1*>)) + 1) - (len (Del (GEN w,the InitS of S),((len w) + 1)))) by A12, A17, FINSEQ_1:36
.= (GEN <*s1*>,q) . (((len (w ^ <*s1*>)) + 1) - (len w)) by A13, MATRLIN:3
.= (GEN <*s1*>,q) . ((((len w) + 1) + 1) - (len w)) by A7, FINSEQ_1:35
.= (GEN <*s1*>,q) . 2 ;
set p2 = GEN <*s2*>,q;
A19: GEN (w ^ <*s2*>),the InitS of S = (Del (GEN w,the InitS of S),((len w) + 1)) ^ (GEN <*s2*>,q) by A3, FSM_1:23;
A20: len (GEN <*s2*>,q) = (len <*s2*>) + 1 by FSM_1:def 2
.= 1 + 1 by FINSEQ_1:56 ;
A21: len (GEN (w ^ <*s2*>),the InitS of S) = len ((Del (GEN w,the InitS of S),((len w) + 1)) ^ (GEN <*s2*>,q)) by A3, FSM_1:23
.= (len (Del (GEN w,the InitS of S),((len w) + 1))) + (len (GEN <*s2*>,q)) by FINSEQ_1:35
.= (len w) + (1 + 1) by A13, A20, MATRLIN:3
.= ((len w) + 1) + 1
.= (len (w ^ <*s2*>)) + 1 by A9, FINSEQ_1:35 ;
(len w) + 1 <= (len (w ^ <*s2*>)) + 1 by A10, NAT_1:11;
then A22: (len (Del (GEN w,the InitS of S),((len w) + 1))) + 1 <= (len (w ^ <*s2*>)) + 1 by A13, MATRLIN:3;
len ((Del (GEN w,the InitS of S),((len w) + 1)) ^ (GEN <*s2*>,q)) = (len (w ^ <*s2*>)) + 1 by A3, A21, FSM_1:23;
then (len (w ^ <*s2*>)) + 1 <= (len (Del (GEN w,the InitS of S),((len w) + 1))) + (len (GEN <*s2*>,q)) by FINSEQ_1:35;
then (GEN (w ^ <*s2*>),the InitS of S) . ((len (w ^ <*s2*>)) + 1) = (GEN <*s2*>,q) . (((len (w ^ <*s2*>)) + 1) - (len (Del (GEN w,the InitS of S),((len w) + 1)))) by A19, A22, FINSEQ_1:36
.= (GEN <*s2*>,q) . (((len (w ^ <*s2*>)) + 1) - (len w)) by A13, MATRLIN:3
.= (GEN <*s2*>,q) . ((((len w) + 1) + 1) - (len w)) by A9, FINSEQ_1:35
.= (GEN <*s2*>,q) . 2 ;
hence (GEN <*s1*>,q) . 2 = (GEN <*s2*>,q) . 2 by A1, A6, A11, A18, Def1; :: thesis: verum