let I, O be non empty set ; :: thesis: for s being Element of I
for M being non empty Moore-SM_Final of I,O st the InitS of M in the FinalS of M holds
the OFun of M . the InitS of M is_result_of s,M
let s be Element of I; :: thesis: for M being non empty Moore-SM_Final of I,O st the InitS of M in the FinalS of M holds
the OFun of M . the InitS of M is_result_of s,M
let M be non empty Moore-SM_Final of I,O; :: thesis: ( the InitS of M in the FinalS of M implies the OFun of M . the InitS of M is_result_of s,M )
assume A1: the InitS of M in the FinalS of M ; :: thesis: the OFun of M . the InitS of M is_result_of s,M
take 1 ; :: according to FSM_2:def 8 :: thesis: for w being FinSequence of I st w . 1 = s holds
( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN w,the InitS of M) . 1) & (GEN w,the InitS of M) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN w,the InitS of M) . n in the FinalS of M ) )
let w be FinSequence of I; :: thesis: ( w . 1 = s implies ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN w,the InitS of M) . 1) & (GEN w,the InitS of M) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN w,the InitS of M) . n in the FinalS of M ) ) )
assume w . 1 = s ; :: thesis: ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN w,the InitS of M) . 1) & (GEN w,the InitS of M) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN w,the InitS of M) . n in the FinalS of M ) )
thus ( ( 1 <= (len w) + 1 implies ( the OFun of M . the InitS of M = the OFun of M . ((GEN w,the InitS of M) . 1) & (GEN w,the InitS of M) . 1 in the FinalS of M ) ) & ( for n being non empty Element of NAT st n < 1 & n <= (len w) + 1 holds
not (GEN w,the InitS of M) . n in the FinalS of M ) ) by A1, FSM_1:def 2, NAT_1:14; :: thesis: verum