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

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