let I be non empty set ; :: thesis: for S being non empty FSM of 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 of 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:7, FINSEQ_1:9;
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

let x be set ; :: 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:3;
A10: i <= 1 + (len w1) by A3, A8, FINSEQ_1:3;
i <= 1 + (len w2) by A3, A8, FINSEQ_1:3;
hence (GEN w1,the InitS of S) . x = (GEN w2,the InitS of S) . x by A1, A2, A9, A10, Def1; :: 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:8; :: according to XBOOLE_0:def 9 :: thesis: verum