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