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

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