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:
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 S1[ 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: S1
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 S1[h] holds
S1[h + 1]
proof
let h be non zero Nat; :: thesis: ( S1[h] implies S1[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: S1[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 ;
A12: h <= (len w1) + 1 by ;
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 ;
A16: h <= len w2 by ;
A17: h <= (len w2) + 1 by ;
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 ;
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 S1[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