for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )