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:9;
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:9;
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;