let I be non empty set ; :: thesis: for S being non empty FSM over I st ( for s1, s2 being Element of I
for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) holds
S is calculating_type
let S be non empty FSM over I; :: thesis: ( ( for s1, s2 being Element of I
for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) implies S is calculating_type )
assume A1: for s1, s2 being Element of I
for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ; :: thesis: S is calculating_type
for j being non zero Element of NAT
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds
(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j

proof

let j be non zero Element of NAT ; :: thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds
(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j
let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j )
assume that
A2: w1 . 1 = w2 . 1 and
A3: j <= (len w1) + 1 and
A4: j <= (len w2) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j
defpred S₁[ Nat] means for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & $1 <= (len w1) + 1 & $1 <= (len w2) + 1 holds
(GEN (w1, the InitS of S)) . $1 = (GEN (w2, the InitS of S)) . $1;
A5: S₁[1]

proof

let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 )
(GEN (w1, the InitS of S)) . 1 = the InitS of S by FSM_1:def 2;
hence ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) by FSM_1:def 2; :: thesis: verum

end;

A6: for h being non zero Nat st S₁[h] holds
S₁[h + 1]

proof

let h be non zero Nat; :: thesis: ( S₁[h] implies S₁[h + 1] )
assume A7: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & h <= (len w1) + 1 & h <= (len w2) + 1 holds
(GEN (w1, the InitS of S)) . h = (GEN (w2, the InitS of S)) . h ; :: thesis: S₁[h + 1]
let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & h + 1 <= (len w1) + 1 & h + 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) )
assume that
A8: w1 . 1 = w2 . 1 and
A9: h + 1 <= (len w1) + 1 and
A10: h + 1 <= (len w2) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1)
A11: h <= len w1 by A9, XREAL_1:6;
A12: h <= (len w1) + 1 by A9, NAT_1:13;
1 <= h by NAT_1:14;
then consider WI being Element of I, QI, QI1 being State of S such that
WI = w1 . h and
A13: QI = (GEN (w1, the InitS of S)) . h and
A14: QI1 = (GEN (w1, the InitS of S)) . (h + 1) and
A15: WI -succ_of QI = QI1 by A11, FSM_1:def 2;
A16: h <= len w2 by A10, XREAL_1:6;
A17: h <= (len w2) + 1 by A10, NAT_1:13;
1 <= h by NAT_1:14;
then consider WI2 being Element of I, QI2, QI12 being State of S such that
WI2 = w2 . h and
A18: QI2 = (GEN (w2, the InitS of S)) . h and
A19: QI12 = (GEN (w2, the InitS of S)) . (h + 1) and
A20: WI2 -succ_of QI2 = QI12 by A16, FSM_1:def 2;
QI = QI2 by A7, A8, A12, A13, A17, A18;
hence (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A14, A15, A19, A20; :: thesis: verum

end;

for j being non zero Nat holds S₁[j] from NAT_1:sch 10(A5, A6);
hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A2, A3, A4; :: thesis: verum

end;

hence S is calculating_type ; :: thesis: verum