let I be non empty set ; :: thesis: for S being non empty FSM over I st S is calculating_type holds
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
let S be non empty FSM over I; :: thesis: ( S is calculating_type implies 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 )
assume A1: S is calculating_type ; :: 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
let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 implies GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable )
assume A2: w1 . 1 = w2 . 1 ; :: thesis: GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
set A = (Seg (1 + (len w1))) /\ (Seg (1 + (len w2)));
( 1 + (len w1) <= 1 + (len w2) or 1 + (len w2) <= 1 + (len w1) ) ;
then A3: ( ( Seg (1 + (len w1)) c= Seg (1 + (len w2)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = Seg (1 + (len w1)) ) or ( Seg (1 + (len w2)) c= Seg (1 + (len w1)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = Seg (1 + (len w2)) ) ) by FINSEQ_1:5, FINSEQ_1:7;
A4: len (GEN (w1, the InitS of S)) = 1 + (len w1) by FSM_1:def 2;
A5: len (GEN (w2, the InitS of S)) = 1 + (len w2) by FSM_1:def 2;
A6: dom (GEN (w1, the InitS of S)) = Seg (1 + (len w1)) by A4, FINSEQ_1:def 3;
A7: dom (GEN (w2, the InitS of S)) = Seg (1 + (len w2)) by A5, FINSEQ_1:def 3;

now :: thesis: for x being object st x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) holds
(GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x

let x be object ; :: thesis: ( x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) implies (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x )
assume A8: x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) ; :: thesis: (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x
then reconsider i = x as Element of NAT ;
A9: i >= 1 by A3, A8, FINSEQ_1:1;
A10: i <= 1 + (len w1) by A3, A8, FINSEQ_1:1;
i <= 1 + (len w2) by A3, A8, FINSEQ_1:1;
hence (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x by A1, A2, A9, A10; :: thesis: verum

end;

hence ( 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 A3, A6, A7, GRFUNC_1:2; :: according to XBOOLE_0:def 9 :: thesis: verum