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 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; :: thesis: verum

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 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; :: thesis: verum