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,1) = Following s
let A be non-empty Circuit of S; :: thesis: for s being State of A holds Following (s,1) = Following s
let s be State of A; :: thesis: Following (s,1) = Following s
0 + 1 = 1 ;
hence Following (s,1) = Following (Following (s,0)) by Th12
.= Following s by Th11 ;
:: thesis: verum