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
B:
now let x be
set ;
:: thesis: ( x in ==>.-relation TS1 implies x in ==>.-relation TS2 )assume B0:
x in ==>.-relation TS1
;
:: thesis: x in ==>.-relation TS2then consider s,
t being
Element of
TS1,
v,
w being
Element of
E ^omega such that B1:
x = [[s,v],[t,w]]
by ThRel9;
s,
v ==>. t,
w,
TS1
by B0, B1, DefRel;
then B2:
s,
v ==>. t,
w,
TS2
by A2, ThDir15;
reconsider s =
s as
Element of
TS2 by A1;
reconsider t =
t as
Element of
TS2 by A1;
thus
x in ==>.-relation TS2
by B1, B2, DefRel;
:: thesis: verum end;
now let x be
set ;
:: thesis: ( x in ==>.-relation TS2 implies x in ==>.-relation TS1 )assume B0:
x in ==>.-relation TS2
;
:: thesis: x in ==>.-relation TS1then consider s,
t being
Element of
TS2,
v,
w being
Element of
E ^omega such that B1:
x = [[s,v],[t,w]]
by ThRel9;
s,
v ==>. t,
w,
TS2
by B0, B1, DefRel;
then B2:
s,
v ==>. t,
w,
TS1
by A2, ThDir15;
reconsider s =
s,
t =
t as
Element of
TS1 by A1;
thus
x in ==>.-relation TS1
by B1, B2, DefRel;
:: thesis: verum end;
hence
==>.-relation TS1 = ==>.-relation TS2
by B, TARSKI:2; :: thesis: verum