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