set cTS = bool the carrier of TS;
defpred S1[ set , set ] means for c being Element of bool the carrier of TS
for i being Element of E ^omega st $1 = [c,i] holds
( len i = 1 & $2 = i -succ_of (c,TS) );
consider tTS being Relation of [:(bool the carrier of TS),(Lex E):],(bool the carrier of TS) such that
A1:
for x being Element of [:(bool the carrier of TS),(Lex E):]
for y being Element of bool the carrier of TS holds
( [x,y] in tTS iff S1[x,y] )
from RELSET_1:sch 2();
set bTS = transition-system(# (bool the carrier of TS),tTS #);
reconsider bTS = transition-system(# (bool the carrier of TS),tTS #) as strict transition-system over Lex E ;
take
bTS
; ( the carrier of bTS = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) )
thus
the carrier of bTS = bool the carrier of TS
; for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )
let S be Subset of TS; for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )
let w be Element of E ^omega ; for T being Subset of TS holds
( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )
let T be Subset of TS; ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )
thus
( [[S,w],T] in the Tran of bTS implies ( len w = 1 & T = w -succ_of (S,TS) ) )
( len w = 1 & T = w -succ_of (S,TS) implies [[S,w],T] in the Tran of bTS )
set x = [S,w];
assume that
A3:
len w = 1
and
A4:
T = w -succ_of (S,TS)
; [[S,w],T] in the Tran of bTS
A5:
now for xc being Element of bool the carrier of TS
for xi being Element of E ^omega st [S,w] = [xc,xi] holds
( len xi = 1 & T = xi -succ_of (xc,TS) )let xc be
Element of
bool the
carrier of
TS;
for xi being Element of E ^omega st [S,w] = [xc,xi] holds
( len xi = 1 & T = xi -succ_of (xc,TS) )let xi be
Element of
E ^omega ;
( [S,w] = [xc,xi] implies ( len xi = 1 & T = xi -succ_of (xc,TS) ) )assume A6:
[S,w] = [xc,xi]
;
( len xi = 1 & T = xi -succ_of (xc,TS) )
xc = S
by A6, XTUPLE_0:1;
hence
(
len xi = 1 &
T = xi -succ_of (
xc,
TS) )
by A3, A4, A6, XTUPLE_0:1;
verum end;
w in Lex E
by A3, Th9;
then reconsider x = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87;
[x,T] in tTS
by A1, A5;
hence
[[S,w],T] in the Tran of bTS
; verum