theorem Th1: :: FSM_2:1

for I being non empty set
for s being Element of I
for S being non empty FSM over I
for q being State of S holds GEN (<*s*>,q) = <*q,( the Tran of S . [q,s])*>