let s, t be TuringStr ; for x being State of s holds [x, the InitS of t] in UnionSt (s,t)
let x be State of s; [x, the InitS of t] in UnionSt (s,t)
set q0 = the InitS of t;
set A = [: the FStates 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 FStates of s,{ the InitS of t}:]
;
hence
[x, the InitS of t] in UnionSt (s,t)
by XBOOLE_0:def 3; verum