theorem Th17: :: FSM_2:17

for I, O being non empty set
for w being FinSequence of I
for i, f being set
for o being Function of {i,f},O
for j being non zero Element of NAT st 1 < j & j <= (len w) + 1 holds
(GEN (w, the InitS of (I -TwoStatesMooreSM (i,f,o)))) . j = f