let E be non empty set ; :: thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system of F1
for TS2 being non empty transition-system of F2 st the carrier of TS1 = the carrier of TS2 & 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 of F1
for TS2 being non empty transition-system of F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let TS1 be non empty transition-system of F1; :: thesis: for TS2 being non empty transition-system of F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
let TS2 be non empty transition-system of F2; :: thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 implies ==>.-relation TS1 = ==>.-relation TS2 )
assume that
A1: the carrier of TS1 = the carrier of TS2 and
A2: the Tran of TS1 = the Tran of TS2 ; :: thesis: ==>.-relation TS1 = ==>.-relation TS2

A3: now

let x be set ; :: thesis: ( x in ==>.-relation TS1 implies x in ==>.-relation TS2 )
assume A4: 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
A5: x = [[s,v],[t,w]] by Th33;
s,v ==>. t,w,TS1 by A4, A5, Def4;
then s,v ==>. t,w,TS2 by A2, Th21;
hence x in ==>.-relation TS2 by A5, Def4; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in ==>.-relation TS2 implies x in ==>.-relation TS1 )
assume A6: 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
A7: x = [[s,v],[t,w]] by Th33;
s,v ==>. t,w,TS2 by A6, A7, Def4;
then s,v ==>. t,w,TS1 by A2, Th21;
hence x in ==>.-relation TS1 by A7, Def4; :: thesis: verum

end;

hence ==>.-relation TS1 = ==>.-relation TS2 by A3, TARSKI:2; :: thesis: verum