:: deftheorem Def9 defines Result FSM_2:def 9 :
for I, O being non empty set
for M being non empty calculating_type halting Moore-SM_Final over I,O
for s being Element of I
for b₅ being Element of O holds
( b₅ = Result (s,M) iff b₅ is_result_of s,M );