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

x in the Tran of bTS2

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

for x being object st x in the Tran of bTS1 holds
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 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; :: thesis: verum

end;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 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; :: thesis: verum

x in the Tran of bTS2

proof

hence
bTS1 = bTS2
by A7, A9, A11, TARSKI:2; :: thesis: verum
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 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; :: thesis: verum

end;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 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; :: thesis: verum