let I, O be non empty set ; :: thesis: for s being Element of I

for M being non empty Moore-SM_Final over 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 over 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 over 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 zero 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 zero 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 zero 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 zero 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

for M being non empty Moore-SM_Final over 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 over 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 over 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 zero 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 zero 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 zero 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 zero 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