theorem Th26: :: FSM_3:26

for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds
==>.-relation TS reduces [x,u],[y,v]