theorem Th71: :: REWRITE3:71

for x, y being object
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]