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

for p being State of t1

for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds

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

let g be Tran-Goal of t1; :: thesis: for p being State of t1

for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds

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

let p be State of t1; :: thesis: for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds

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

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

assume that

A1: p <> the AcceptS of t1 and

A2: g = the Tran of t1 . [p,y] ; :: thesis: the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)]

set q0 = the InitS of t2;

set x = [[p, the InitS of t2],y];

the InitS of t2 in { the InitS of t2} by TARSKI:def 1;

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

then A3: [p, the InitS of t2] 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 = [[p, the InitS of t2],y] as Element of [:(UnionSt (t1,t2)),( the Symbols of t1 \/ the Symbols of t2):] by A3, ZFMISC_1:def 2;

A4: FirstTuringState xx = ([[p, the InitS of t2],y] `1) `1

.= [p, the InitS of t2] `1

.= p ;

A5: FirstTuringSymbol xx = [[p, the InitS of t2],y] `2 by Def27

.= y ;

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

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

.= FirstTuringTran (t1,t2,( the Tran of t1 . [p,y])) by A1, A4, A5, Def29

.= [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)] by A2 ; :: thesis: verum

for p being State of t1

for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds

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

let g be Tran-Goal of t1; :: thesis: for p being State of t1

for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds

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

let p be State of t1; :: thesis: for y being Symbol of t1 st p <> the AcceptS of t1 & g = the Tran of t1 . [p,y] holds

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

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

assume that

A1: p <> the AcceptS of t1 and

A2: g = the Tran of t1 . [p,y] ; :: thesis: the Tran of (t1 ';' t2) . [[p, the InitS of t2],y] = [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)]

set q0 = the InitS of t2;

set x = [[p, the InitS of t2],y];

the InitS of t2 in { the InitS of t2} by TARSKI:def 1;

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

then A3: [p, the InitS of t2] 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 = [[p, the InitS of t2],y] as Element of [:(UnionSt (t1,t2)),( the Symbols of t1 \/ the Symbols of t2):] by A3, ZFMISC_1:def 2;

A4: FirstTuringState xx = ([[p, the InitS of t2],y] `1) `1

.= [p, the InitS of t2] `1

.= p ;

A5: FirstTuringSymbol xx = [[p, the InitS of t2],y] `2 by Def27

.= y ;

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

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

.= FirstTuringTran (t1,t2,( the Tran of t1 . [p,y])) by A1, A4, A5, Def29

.= [[(g `1_3), the InitS of t2],(g `2_3),(g `3_3)] by A2 ; :: thesis: verum