theorem :: REWRITE3:65

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