:: deftheorem defines -succ_of FSM_1:def 1 :
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for s being Element of IAlph
for q being State of fsm holds s -succ_of q = the Tran of fsm . [q,s];