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 the InitS of M in the FinalS of M holds
the OFun of M . the InitS of M is_result_of s,M