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

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