the carrier of (tfsm1 -Mealy_union tfsm2) = the carrier of tfsm1 \/ the carrier of tfsm2 by Def24;
hence ( not tfsm1 -Mealy_union tfsm2 is empty & tfsm1 -Mealy_union tfsm2 is finite ) ; :: thesis: verum