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;

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

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(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;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