theorem Th29: :: FSM_3:29

for X being set
for E being non empty set
for v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)