let I be non empty set ; :: thesis: for S being non empty FSM of 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 of 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: S is calculating_type
let j be non empty 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 A3, A5, FINSEQ_1:3;
j in dom (GEN w2,the InitS of S) by A4, A6, A7, FINSEQ_1:3;
then A9: j in (dom (GEN w1,the InitS of S)) /\ (dom (GEN w2,the InitS of S)) by A8, XBOOLE_0:def 4;
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 ) by XBOOLE_0:def 9;
then GEN w1,the InitS of S tolerates GEN w2,the InitS of S by PARTFUN1:135;
hence (GEN w1,the InitS of S) . j = (GEN w2,the InitS of S) . j by A9, PARTFUN1:def 6; :: thesis: verum