let I, O be non empty set ; 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; 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; ( 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
; the OFun of M . the InitS of M is_result_of s,M
take
1
; FSM_2:def 8 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; ( 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
; ( ( 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; verum