let s, t be TuringStr ; :: thesis: for x being Element of UnionSt (s,t) ex x1 being State of s ex x2 being State of t st x = [x1,x2]
let x be Element of UnionSt (s,t); :: thesis: ex x1 being State of s ex x2 being State of t st x = [x1,x2]
set q0 = the InitS of t;
set p1 = the AcceptS of s;
set A = [: the FStates of s,{ the InitS of t}:];
set B = [:{ the AcceptS of s}, the FStates of t:];

per cases ( x in [: the FStates of s,{ the InitS of t}:] or x in [:{ the AcceptS of s}, the FStates of t:] ) by XBOOLE_0:def 3;

suppose x in [: the FStates of s,{ the InitS of t}:] ; :: thesis: ex x1 being State of s ex x2 being State of t st x = [x1,x2]

then consider x1 being State of s, x2 being Element of { the InitS of t} such that
A1: x = [x1,x2] by DOMAIN_1:1;
take x1 ; :: thesis: ex x2 being State of t st x = [x1,x2]
take the InitS of t ; :: thesis: x = [x1, the InitS of t]
thus x = [x1, the InitS of t] by A1, TARSKI:def 1; :: thesis: verum

end;

suppose x in [:{ the AcceptS of s}, the FStates of t:] ; :: thesis: ex x1 being State of s ex x2 being State of t st x = [x1,x2]

then consider x1 being Element of { the AcceptS of s}, x2 being State of t such that
A2: x = [x1,x2] by DOMAIN_1:1;
take the AcceptS of s ; :: thesis: ex x2 being State of t st x = [ the AcceptS of s,x2]
take x2 ; :: thesis: x = [ the AcceptS of s,x2]
thus x = [ the AcceptS of s,x2] by A2, TARSKI:def 1; :: thesis: verum

end;

end;