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)

proof

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:47;
then len (<*s*> ^ w) = 1 by FINSEQ_1:56;
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;

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