set cTS = bool the carrier of TS;
let bTS1, bTS2 be strict transition-system over Lex E; ( the carrier of bTS1 = 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 bTS1 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) & the carrier of bTS2 = 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 bTS2 iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) implies bTS1 = bTS2 )
assume that
A7:
the carrier of bTS1 = bool the carrier of TS
and
A8:
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 bTS1 iff ( len w = 1 & T = w -succ_of (S,TS) ) )
and
A9:
the carrier of bTS2 = bool the carrier of TS
and
A10:
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 bTS2 iff ( len w = 1 & T = w -succ_of (S,TS) ) )
; bTS1 = bTS2
A11:
for x being object st x in the Tran of bTS2 holds
x in the Tran of bTS1
proof
let x be
object ;
( x in the Tran of bTS2 implies x in the Tran of bTS1 )
assume A12:
x in the
Tran of
bTS2
;
x in the Tran of bTS1
then consider xbi,
xc being
object such that A13:
x = [xbi,xc]
and A14:
xbi in [:(bool the carrier of TS),(Lex E):]
and A15:
xc in bool the
carrier of
TS
by A9, RELSET_1:2;
reconsider xc =
xc as
Element of
bool the
carrier of
TS by A15;
[:(bool the carrier of TS),(Lex E):] c= [:(bool the carrier of TS),(Lex E):]
;
then consider xb,
xi being
object such that A16:
xbi = [xb,xi]
and A17:
xb in bool the
carrier of
TS
and A18:
xi in Lex E
by A14, RELSET_1:2;
reconsider xb =
xb as
Element of
bool the
carrier of
TS by A17;
reconsider xi =
xi as
Element of
Lex E by A18;
reconsider xe =
xi as
Element of
E ^omega ;
A19:
len xe = 1
by Th9;
xc = xi -succ_of (
xb,
TS)
by A10, A12, A13, A16;
hence
x in the
Tran of
bTS1
by A8, A13, A16, A19;
verum
end;
for x being object st x in the Tran of bTS1 holds
x in the Tran of bTS2
proof
let x be
object ;
( x in the Tran of bTS1 implies x in the Tran of bTS2 )
assume A20:
x in the
Tran of
bTS1
;
x in the Tran of bTS2
then consider xbi,
xc being
object such that A21:
x = [xbi,xc]
and A22:
xbi in [:(bool the carrier of TS),(Lex E):]
and A23:
xc in bool the
carrier of
TS
by A7, RELSET_1:2;
reconsider xc =
xc as
Element of
bool the
carrier of
TS by A23;
[:(bool the carrier of TS),(Lex E):] c= [:(bool the carrier of TS),(Lex E):]
;
then consider xb,
xi being
object such that A24:
xbi = [xb,xi]
and A25:
xb in bool the
carrier of
TS
and A26:
xi in Lex E
by A22, RELSET_1:2;
reconsider xb =
xb as
Element of
bool the
carrier of
TS by A25;
reconsider xi =
xi as
Element of
Lex E by A26;
reconsider xe =
xi as
Element of
E ^omega ;
A27:
len xe = 1
by Th9;
xc = xi -succ_of (
xb,
TS)
by A8, A20, A21, A24;
hence
x in the
Tran of
bTS2
by A10, A21, A24, A27;
verum
end;
hence
bTS1 = bTS2
by A7, A9, A11, TARSKI:2; verum