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 holds Following s,0 = s
let A be non-empty Circuit of non-empty ; :: thesis: for s being State of holds Following s,0 = s
let s be State of ; :: thesis: Following s,0 = s
ex f being Function of NAT , product the Sorts of A st
( Following s,0 = f . 0 & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) by Def8;
hence Following s,0 = s ; :: thesis: verum