let E be non empty set ; :: thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let F1, F2 be Subset of (E ^omega); :: thesis: for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let TS1 be non empty transition-system over F1; :: thesis: for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let TS2 be non empty transition-system over F2; :: thesis: ( the Tran of TS1 = the Tran of TS2 implies ==>.-relation TS1 = ==>.-relation TS2 )
assume A1: the Tran of TS1 = the Tran of TS2 ; :: thesis: ==>.-relation TS1 = ==>.-relation TS2
A2: now :: thesis: for x being object st x in ==>.-relation TS1 holds
x in ==>.-relation TS2
let x be object ; :: thesis: ( x in ==>.-relation TS1 implies x in ==>.-relation TS2 )
assume A3: x in ==>.-relation TS1 ; :: thesis: x in ==>.-relation TS2
then consider s, t being Element of TS1, v, w being Element of E ^omega such that
A4: x = [[s,v],[t,w]] by Th33;
s,v ==>. t,w,TS1 by A3, A4, Def4;
then s,v ==>. t,w,TS2 by A1, Th21;
hence x in ==>.-relation TS2 by A4, Def4; :: thesis: verum
end;
now :: thesis: for x being object st x in ==>.-relation TS2 holds
x in ==>.-relation TS1
let x be object ; :: thesis: ( x in ==>.-relation TS2 implies x in ==>.-relation TS1 )
assume A5: x in ==>.-relation TS2 ; :: thesis: x in ==>.-relation TS1
then consider s, t being Element of TS2, v, w being Element of E ^omega such that
A6: x = [[s,v],[t,w]] by Th33;
s,v ==>. t,w,TS2 by A5, A6, Def4;
then s,v ==>. t,w,TS1 by A1, Th21;
hence x in ==>.-relation TS1 by A6, Def4; :: thesis: verum
end;
hence ==>.-relation TS1 = ==>.-relation TS2 by A2, TARSKI:2; :: thesis: verum