let S be one-gate ManySortedSign ; :: thesis: for A being one-gate Circuit of S
for s being State of A holds Result s = Following s
let A be one-gate Circuit of S; :: thesis: for s being State of A holds Result s = Following s
let s be State of A; :: thesis: Result s = Following s
A1: Following s = Following (s,1) by FACIRC_1:14;
( s is stabilizing & Following s is stable ) by Def2, Th19;
hence Result s = Following s by A1, Def4; :: thesis: verum