let I, O be non empty set ; :: thesis: for s being Element of I
for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1
let s be Element of I; :: thesis: for f being Function of {0,1},O holds Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1
let f be Function of {0,1},O; :: thesis: Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1
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;

now :: thesis: ex m being non zero Element of NAT st
for w being FinSequence of I st w . 1 = s holds
( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) )

take m = m; :: thesis: for w being FinSequence of I st w . 1 = s holds
( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) )
let w be FinSequence of I; :: thesis: ( w . 1 = s implies ( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) )
assume A6: w . 1 = s ; :: thesis: ( ( m <= (len w) + 1 implies ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) )

hereby :: thesis: for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f))

assume m <= (len w) + 1 ; :: thesis: ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) )
then (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A4, A6;
hence ( f . 1 = the OFun of (I -TwoStatesMooreSM (0,1,f)) . ((GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m) & (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . m in the FinalS of (I -TwoStatesMooreSM (0,1,f)) ) by A2, A3, TARSKI:def 1; :: thesis: verum

end;

thus for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of (I -TwoStatesMooreSM (0,1,f)))) . n in the FinalS of (I -TwoStatesMooreSM (0,1,f)) by A5, A6; :: thesis: verum

end;

then f . 01 is_result_of s,I -TwoStatesMooreSM (0,1,f) ;
hence Result (s,(I -TwoStatesMooreSM (0,1,f))) = f . 1 by Def9; :: thesis: verum