let s, t be TuringStr ; :: thesis: for x being State of s holds [x,the InitS of t] in UnionSt s,t
let x be State of s; :: thesis: [x,the InitS of t] in UnionSt s,t
set q0 = the InitS of t;
set A = [:the States of s,{the InitS of t}:];
reconsider q = the InitS of t as Element of {the InitS of t} by TARSKI:def 1;
[x,q] in [:the States of s,{the InitS of t}:] ;
hence [x,the InitS of t] in UnionSt s,t by XBOOLE_0:def 3; :: thesis: verum