let t1, t2 be TuringStr ; :: thesis: for g being Tran-Goal of t2

for q being State of t2

for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds

the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

let g be Tran-Goal of t2; :: thesis: for q being State of t2

for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds

the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

let q be State of t2; :: thesis: for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds

the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

let y be Symbol of t2; :: thesis: ( g = the Tran of t2 . [q,y] implies the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)] )

assume A1: g = the Tran of t2 . [q,y] ; :: thesis: the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

set pF = the AcceptS of t1;

set x = [[ the AcceptS of t1,q],y];

the AcceptS of t1 in { the AcceptS of t1} by TARSKI:def 1;

then [ the AcceptS of t1,q] in [:{ the AcceptS of t1}, the FStates of t2:] by ZFMISC_1:def 2;

then A2: [ the AcceptS of t1,q] in [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:] by XBOOLE_0:def 3;

y in the Symbols of t1 \/ the Symbols of t2 by XBOOLE_0:def 3;

then reconsider xx = [[ the AcceptS of t1,q],y] as Element of [:(UnionSt (t1,t2)),( the Symbols of t1 \/ the Symbols of t2):] by A2, ZFMISC_1:def 2;

A3: SecondTuringState xx = ([[ the AcceptS of t1,q],y] `1) `2

.= q ;

A4: SecondTuringSymbol xx = [[ the AcceptS of t1,q],y] `2 by Def28

.= y ;

thus the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = (UnionTran (t1,t2)) . xx by Def31

.= Uniontran (t1,t2,xx) by Def30

.= SecondTuringTran (t1,t2,( the Tran of t2 . [q,y])) by A3, A4, Def29

.= [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)] by A1 ; :: thesis: verum

for q being State of t2

for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds

the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

let g be Tran-Goal of t2; :: thesis: for q being State of t2

for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds

the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

let q be State of t2; :: thesis: for y being Symbol of t2 st g = the Tran of t2 . [q,y] holds

the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

let y be Symbol of t2; :: thesis: ( g = the Tran of t2 . [q,y] implies the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)] )

assume A1: g = the Tran of t2 . [q,y] ; :: thesis: the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)]

set pF = the AcceptS of t1;

set x = [[ the AcceptS of t1,q],y];

the AcceptS of t1 in { the AcceptS of t1} by TARSKI:def 1;

then [ the AcceptS of t1,q] in [:{ the AcceptS of t1}, the FStates of t2:] by ZFMISC_1:def 2;

then A2: [ the AcceptS of t1,q] in [: the FStates of t1,{ the InitS of t2}:] \/ [:{ the AcceptS of t1}, the FStates of t2:] by XBOOLE_0:def 3;

y in the Symbols of t1 \/ the Symbols of t2 by XBOOLE_0:def 3;

then reconsider xx = [[ the AcceptS of t1,q],y] as Element of [:(UnionSt (t1,t2)),( the Symbols of t1 \/ the Symbols of t2):] by A2, ZFMISC_1:def 2;

A3: SecondTuringState xx = ([[ the AcceptS of t1,q],y] `1) `2

.= q ;

A4: SecondTuringSymbol xx = [[ the AcceptS of t1,q],y] `2 by Def28

.= y ;

thus the Tran of (t1 ';' t2) . [[ the AcceptS of t1,q],y] = (UnionTran (t1,t2)) . xx by Def31

.= Uniontran (t1,t2,xx) by Def30

.= SecondTuringTran (t1,t2,( the Tran of t2 . [q,y])) by A3, A4, Def29

.= [[ the AcceptS of t1,(g `1_3)],(g `2_3),(g `3_3)] by A1 ; :: thesis: verum