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