theorem Th11: :: FSM_3:11

for E being non empty set
for TS being transition-system over Lex E st the Tran of TS is Function holds
TS is deterministic