theorem Th81: :: REWRITE3:81

for x1, x2, y1, y2 being object
for E being non empty set
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 carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2 by Th34;