theorem Th2: :: FSM_2:2

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