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 FStates of t1,{ the InitS of t2}:];
set B = [:{ the AcceptS of t1}, the FStates of t2:];
reconsider q = the InitS of t2 as Element of { the InitS of t2} by TARSKI:def 1;
reconsider p = the AcceptS of t1 as Element of { the AcceptS of t1} by TARSKI:def 1;
[ the InitS of t1,q] in [: the FStates 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)
[p, the AcceptS of t2] in [:{ the AcceptS of t1}, the FStates of t2:] ;
hence [ the AcceptS of t1, the AcceptS of t2] in UnionSt (t1,t2) by XBOOLE_0:def 3; :: thesis: verum