let I, O be non empty set ; :: thesis:
let s be Element of I; :: thesis:
let f be Function of {0,1},O; :: thesis:
set M = I -TwoStatesMooreSM (0,1,f);
reconsider 01 = 1 as Element of {0,1} by TARSKI:def 2;
A1: s leads_to_final_state_of I -TwoStatesMooreSM (0,1,f) by Def6;
A2: the FinalS of (I -TwoStatesMooreSM (0,1,f)) = {1} by Def7;
A3: the OFun of (I -TwoStatesMooreSM (0,1,f)) = f by Def7;
consider m being non zero Element of NAT such that
A4: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) and
A5: for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . j in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A1, Th18;

end;

end;