for I, O being non empty set
for s being Element of I
for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex t being Element of O st t is_result_of s,M