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

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;

end;

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

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