set St = UnionSt T1,T2;
set Sym = the Symbols of T1 \/ the Symbols of T2;
reconsider p0 = [the InitS of T1,the InitS of T2] as Element of UnionSt T1,T2 by Th44;
reconsider q1 = [the AcceptS of T1,the AcceptS of T2] as Element of UnionSt T1,T2 by Th44;
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 States 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 States 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