let x1, x2, y1, y2 be object ; for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let E be non empty set ; for F1, F2 being Subset of (E ^omega)
for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let F1, F2 be Subset of (E ^omega); for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let TS1 be transition-system over F1; for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let TS2 be transition-system over F2; ( the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 implies x1,x2 ==>. y1,y2,TS2 )
assume that
A1:
the Tran of TS1 = the Tran of TS2
and
A2:
x1,x2 ==>. y1,y2,TS1
; x1,x2 ==>. y1,y2,TS2
consider v, w being Element of E ^omega such that
A3:
( v = y2 & x1,w -->. y1,TS1 & x2 = w ^ v )
by A2;
take
v
; REWRITE3:def 3 ex w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v )
take
w
; ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v )
thus
( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v )
by A1, A3; verum