set cTS = bool the carrier of TS;
let bTS1, bTS2 be strict transition-system over Lex E; :: thesis: ( 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) ) ) ; :: thesis: 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 ; :: thesis: ( x in the Tran of bTS2 implies x in the Tran of bTS1 )
assume A12: x in the Tran of bTS2 ; :: thesis: 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 ;
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 ;
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; :: thesis: 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 ; :: thesis: ( x in the Tran of bTS1 implies x in the Tran of bTS2 )
assume A20: x in the Tran of bTS1 ; :: thesis: 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 ;
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 ;
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; :: thesis: verum
end;
hence bTS1 = bTS2 by ; :: thesis: verum