let I be non empty set ; :: thesis: for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds
S is calculating_type

let S be non empty FSM over I; :: thesis: ( ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) implies S is calculating_type )

assume A1: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ; :: thesis:
let j be non zero Element of NAT ; :: according to FSM_2:def 1 :: 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
A5: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def 3
.= Seg ((len w1) + 1) by FSM_1:def 2 ;
A6: dom (GEN (w2, the InitS of S)) = Seg (len (GEN (w2, the InitS of S))) by FINSEQ_1:def 3
.= Seg ((len w2) + 1) by FSM_1:def 2 ;
A7: 1 <= j by NAT_1:14;
then A8: j in dom (GEN (w1, the InitS of S)) by ;
j in dom (GEN (w2, the InitS of S)) by ;
then A9: j in (dom (GEN (w1, the InitS of S))) /\ (dom (GEN (w2, the InitS of S))) by ;
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by A1, A2;
then ( GEN (w1, the InitS of S) c= GEN (w2, the InitS of S) or GEN (w2, the InitS of S) c= GEN (w1, the InitS of S) ) ;
then GEN (w1, the InitS of S) tolerates GEN (w2, the InitS of S) by PARTFUN1:54;
hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by ; :: thesis: verum