set St = UnionSt (T1,T2);
reconsider q1 = [ the AcceptS of T1, the AcceptS of T2] as Element of UnionSt (T1,T2) by Th39;
reconsider p0 = [ the InitS of T1, the InitS of T2] as Element of UnionSt (T1,T2) by Th39;
set Sym = the Symbols of T1 \/ the Symbols of T2;
take TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) ; :: thesis: ( the Symbols of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = the Symbols of T1 \/ the Symbols of T2 & the FStates of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = UnionSt (T1,T2) & the Tran of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = UnionTran (T1,T2) & the InitS of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = [ the InitS of T1, the InitS of T2] & the AcceptS of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = [ the AcceptS of T1, the AcceptS of T2] )
thus ( the Symbols of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = the Symbols of T1 \/ the Symbols of T2 & the FStates of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = UnionSt (T1,T2) & the Tran of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = UnionTran (T1,T2) & the InitS of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = [ the InitS of T1, the InitS of T2] & the AcceptS of TuringStr(# ( the Symbols of T1 \/ the Symbols of T2),(UnionSt (T1,T2)),(UnionTran (T1,T2)),p0,q1 #) = [ the AcceptS of T1, the AcceptS of T2] ) ; :: thesis: verum