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