let O, I 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 InitS of (I -TwoStatesMooreSM 0 ,1,f) = 0 & the FinalS of (I -TwoStatesMooreSM 0 ,1,f) = {1} & not 0 in {1} & the OFun of (I -TwoStatesMooreSM 0 ,1,f) = f ) by Def7, TARSKI:def 1;
then consider m being non empty Element of NAT such that
A3: 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
A4: for w being FinSequence of I
for j being non empty 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

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 empty 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 empty 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 A5: 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 empty 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 empty 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 A3, A5;
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, TARSKI:def 1; :: thesis: verum

end;

thus for n being non empty 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 A4, A5; :: thesis: verum

end;

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