set Oftfsm1 = the OFun of tfsm1;
set Oftfsm2 = the OFun of tfsm2;
set Trtfsm1 = the Tran of tfsm1;
set Trtfsm2 = the Tran of tfsm2;
set Stfsm1 = the carrier of tfsm1;
set Stfsm2 = the carrier of tfsm2;
set Tr = the Tran of tfsm1 +* the Tran of tfsm2;
set Of = the OFun of tfsm1 +* the OFun of tfsm2;
reconsider S = the carrier of tfsm1 \/ the carrier of tfsm2 as non empty set ;
( rng the Tran of tfsm1 c= the carrier of tfsm1 & rng the Tran of tfsm2 c= the carrier of tfsm2 ) by RELAT_1:def 19;
then A1: ( rng ( the Tran of tfsm1 +* the Tran of tfsm2) c= (rng the Tran of tfsm1) \/ (rng the Tran of tfsm2) & (rng the Tran of tfsm1) \/ (rng the Tran of tfsm2) c= the carrier of tfsm1 \/ the carrier of tfsm2 ) by FUNCT_4:18, XBOOLE_1:13;
( dom the OFun of tfsm1 = [: the carrier of tfsm1,IAlph:] & dom the OFun of tfsm2 = [: the carrier of tfsm2,IAlph:] ) by FUNCT_2:def 1;
then A2: dom ( the OFun of tfsm1 +* the OFun of tfsm2) = [: the carrier of tfsm1,IAlph:] \/ [: the carrier of tfsm2,IAlph:] by FUNCT_4:def 1
.= [:( the carrier of tfsm1 \/ the carrier of tfsm2),IAlph:] by ZFMISC_1:120 ;
( rng the OFun of tfsm1 c= OAlph & rng the OFun of tfsm2 c= OAlph ) by RELAT_1:def 19;
then ( rng ( the OFun of tfsm1 +* the OFun of tfsm2) c= (rng the OFun of tfsm1) \/ (rng the OFun of tfsm2) & (rng the OFun of tfsm1) \/ (rng the OFun of tfsm2) c= OAlph \/ OAlph ) by FUNCT_4:18, XBOOLE_1:13;
then reconsider Of = the OFun of tfsm1 +* the OFun of tfsm2 as Function of [:S,IAlph:],OAlph by A2, FUNCT_2:4, XBOOLE_1:1;
( dom the Tran of tfsm1 = [: the carrier of tfsm1,IAlph:] & dom the Tran of tfsm2 = [: the carrier of tfsm2,IAlph:] ) by FUNCT_2:def 1;
then dom ( the Tran of tfsm1 +* the Tran of tfsm2) = [: the carrier of tfsm1,IAlph:] \/ [: the carrier of tfsm2,IAlph:] by FUNCT_4:def 1
.= [:( the carrier of tfsm1 \/ the carrier of tfsm2),IAlph:] by ZFMISC_1:120 ;
then reconsider Tr = the Tran of tfsm1 +* the Tran of tfsm2 as Function of [:S,IAlph:],S by A1, FUNCT_2:4, XBOOLE_1:1;
reconsider IS = the InitS of tfsm1 as Element of S by XBOOLE_0:def 3;
take Mealy-FSM(# S,Tr,Of,IS #) ; :: thesis: ( the carrier of Mealy-FSM(# S,Tr,Of,IS #) = the carrier of tfsm1 \/ the carrier of tfsm2 & the Tran of Mealy-FSM(# S,Tr,Of,IS #) = the Tran of tfsm1 +* the Tran of tfsm2 & the OFun of Mealy-FSM(# S,Tr,Of,IS #) = the OFun of tfsm1 +* the OFun of tfsm2 & the InitS of Mealy-FSM(# S,Tr,Of,IS #) = the InitS of tfsm1 )
thus ( the carrier of Mealy-FSM(# S,Tr,Of,IS #) = the carrier of tfsm1 \/ the carrier of tfsm2 & the Tran of Mealy-FSM(# S,Tr,Of,IS #) = the Tran of tfsm1 +* the Tran of tfsm2 & the OFun of Mealy-FSM(# S,Tr,Of,IS #) = the OFun of tfsm1 +* the OFun of tfsm2 & the InitS of Mealy-FSM(# S,Tr,Of,IS #) = the InitS of tfsm1 ) ; :: thesis: verum