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,2 = Following (Following s)
let A be non-empty Circuit of non-empty ; :: thesis: for s being State of holds Following s,2 = Following (Following s)
let s be State of ; :: 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