set c = Ctfsm;
set rtfsm = the_reduction_of Ctfsm;
A1:
the InitS of Ctfsm in the InitS of (the_reduction_of Ctfsm)
by Def18;
assume
not the_reduction_of Ctfsm is connected
; contradiction
then consider Q being State of (the_reduction_of Ctfsm) such that
A2:
not Q is accessible
;
A3:
the carrier of (the_reduction_of Ctfsm) = final_states_partition Ctfsm
by Def18;
then reconsider Q9 = Q as Subset of Ctfsm by TARSKI:def 3;
Q in the carrier of (the_reduction_of Ctfsm)
;
then
Q9 in final_states_partition Ctfsm
by Def18;
then consider q being Element of Ctfsm such that
A4:
q in Q
by FINSEQ_4:87;
q is accessible
by Def22;
then consider w being FinSequence of IAlph such that
A5:
the InitS of Ctfsm,w -leads_to q
;
1 <= (len w) + 1
by NAT_1:11;
then A6:
(len w) + 1 in Seg ((len w) + 1)
by FINSEQ_1:1;
then
(len w) + 1 in Seg (len (( the InitS of (the_reduction_of Ctfsm),w) -admissible))
by Def2;
then
(len w) + 1 in dom (( the InitS of (the_reduction_of Ctfsm),w) -admissible)
by FINSEQ_1:def 3;
then A7:
(( the InitS of (the_reduction_of Ctfsm),w) -admissible) . ((len w) + 1) in the carrier of (the_reduction_of Ctfsm)
by FINSEQ_2:11;
then reconsider QQ = (( the InitS of (the_reduction_of Ctfsm),w) -admissible) . ((len w) + 1) as Subset of Ctfsm by A3;
A8:
( Q9 = QQ or Q9 misses QQ )
by A3, A7, EQREL_1:def 4;
(( the InitS of Ctfsm,w) -admissible) . ((len w) + 1) = q
by A5;
then
q in (( the InitS of (the_reduction_of Ctfsm),w) -admissible) . ((len w) + 1)
by A1, A6, Th40;
then
the InitS of (the_reduction_of Ctfsm),w -leads_to Q
by A4, A8, XBOOLE_0:3;
hence
contradiction
by A2; verum