:: deftheorem Def24 defines -Mealy_union FSM_1:def 24 :
for IAlph being set
for OAlph being non empty set
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for b₅ being strict Mealy-FSM over IAlph,OAlph holds
( b₅ = tfsm1 -Mealy_union tfsm2 iff ( the carrier of b₅ = the carrier of tfsm1 \/ the carrier of tfsm2 & the Tran of b₅ = the Tran of tfsm1 +* the Tran of tfsm2 & the OFun of b₅ = the OFun of tfsm1 +* the OFun of tfsm2 & the InitS of b₅ = the InitS of tfsm1 ) );