theorem :: REWRITE3:45

for x, y1, y2, z1, z2 being object
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )