let s, t be TuringStr ; :: thesis: for x being State of t holds [ the AcceptS of s,x] in UnionSt (s,t)

let x be State of t; :: thesis: [ the AcceptS of s,x] in UnionSt (s,t)

set p1 = the AcceptS of s;

set B = [:{ the AcceptS of s}, the FStates of t:];

reconsider p = the AcceptS of s as Element of { the AcceptS of s} by TARSKI:def 1;

[p,x] in [:{ the AcceptS of s}, the FStates of t:] ;

hence [ the AcceptS of s,x] in UnionSt (s,t) by XBOOLE_0:def 3; :: thesis: verum

let x be State of t; :: thesis: [ the AcceptS of s,x] in UnionSt (s,t)

set p1 = the AcceptS of s;

set B = [:{ the AcceptS of s}, the FStates of t:];

reconsider p = the AcceptS of s as Element of { the AcceptS of s} by TARSKI:def 1;

[p,x] in [:{ the AcceptS of s}, the FStates of t:] ;

hence [ the AcceptS of s,x] in UnionSt (s,t) by XBOOLE_0:def 3; :: thesis: verum