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 )],(g `2 ),(g `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 )],(g `2 ),(g `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 )],(g `2 ),(g `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 )],(g `2 ),(g `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 )],(g `2 ),(g `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] `2 by MCART_1:def 1
.= q by MCART_1:def 2 ;
A4: SecondTuringSymbol xx = xx `2 by Def29
.= y by MCART_1:def 2 ;
thus the Tran of (t1 ';' t2) . [[the AcceptS of t1,q],y] = (UnionTran t1,t2) . xx by Def32
.= Uniontran t1,t2,xx by Def31
.= SecondTuringTran t1,t2,(the Tran of t2 . [q,y]) by A3, A4, Def30
.= [[the AcceptS of t1,(g `1 )],(g `2 ),(g `3 )] by A1 ; :: thesis: verum