let s be Element of I; :: according to FSM_2:def 6 :: thesis: s leads_to_final_state_of I -TwoStatesMooreSM (i,f,o)

{i,f} = the carrier of (I -TwoStatesMooreSM (i,f,o)) by Def7;

then reconsider q = f as State of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def 2;

take q ; :: according to FSM_2:def 5 :: thesis: ( q is_accessible_via s & q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) )

thus q is_accessible_via s :: thesis: q in the FinalS of (I -TwoStatesMooreSM (i,f,o))

hence q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def 1; :: thesis: verum

{i,f} = the carrier of (I -TwoStatesMooreSM (i,f,o)) by Def7;

then reconsider q = f as State of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def 2;

take q ; :: according to FSM_2:def 5 :: thesis: ( q is_accessible_via s & q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) )

thus q is_accessible_via s :: thesis: q in the FinalS of (I -TwoStatesMooreSM (i,f,o))

proof

the FinalS of (I -TwoStatesMooreSM (i,f,o)) = {f}
by Def7;
take w = <*> I; :: according to FSM_2:def 2 :: thesis: the InitS of (I -TwoStatesMooreSM (i,f,o)),<*s*> ^ w -leads_to q

<*s*> ^ w = <*s*> by FINSEQ_1:34;

then len (<*s*> ^ w) = 1 by FINSEQ_1:39;

hence (GEN ((<*s*> ^ w), the InitS of (I -TwoStatesMooreSM (i,f,o)))) . ((len (<*s*> ^ w)) + 1) = q by Th17; :: according to FSM_1:def 3 :: thesis: verum

end;<*s*> ^ w = <*s*> by FINSEQ_1:34;

then len (<*s*> ^ w) = 1 by FINSEQ_1:39;

hence (GEN ((<*s*> ^ w), the InitS of (I -TwoStatesMooreSM (i,f,o)))) . ((len (<*s*> ^ w)) + 1) = q by Th17; :: according to FSM_1:def 3 :: thesis: verum

hence q in the FinalS of (I -TwoStatesMooreSM (i,f,o)) by TARSKI:def 1; :: thesis: verum