let S be non empty non void Circuit-like ManySortedSign ; :: thesis: for A being non-empty Circuit of non-empty
for s being State of
for n being Nat holds Following s,(n + 1) = Following (Following s),n
let A be non-empty Circuit of non-empty ; :: thesis: for s being State of
for n being Nat holds Following s,(n + 1) = Following (Following s),n
let s be State of ; :: thesis: for n being Nat holds Following s,(n + 1) = Following (Following s),n
let n be Nat; :: thesis: Following s,(n + 1) = Following (Following s),n
Following s,(n + 1) = Following (Following s,1),n by Th13;
hence Following s,(n + 1) = Following (Following s),n by Th14; :: thesis: verum