let t1, t2 be TuringStr ; :: thesis: ( [the InitS of t1,the InitS of t2] in UnionSt t1,t2 & [the AcceptS of t1,the AcceptS of t2] in UnionSt t1,t2 )
set p0 = the InitS of t1;
set q0 = the InitS of t2;
set p1 = the AcceptS of t1;
set q1 = the AcceptS of t2;
set A = [:the States of t1,{the InitS of t2}:];
set B = [:{the AcceptS of t1},the States of t2:];
reconsider q = the InitS of t2 as Element of {the InitS of t2} by TARSKI:def 1;
[the InitS of t1,q] in [:the States of t1,{the InitS of t2}:] ;
hence [the InitS of t1,the InitS of t2] in UnionSt t1,t2 by XBOOLE_0:def 3; :: thesis: [the AcceptS of t1,the AcceptS of t2] in UnionSt t1,t2
reconsider p = the AcceptS of t1 as Element of {the AcceptS of t1} by TARSKI:def 1;
[p,the AcceptS of t2] in [:{the AcceptS of t1},the States of t2:] ;
hence [the AcceptS of t1,the AcceptS of t2] in UnionSt t1,t2 by XBOOLE_0:def 3; :: thesis: verum