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 holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q