theorem Th16: :: FACIRC_1:16

for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)