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: s is stabilizing by Def2;
A2: Following s is stable by Th20;
Following s = Following s,1 by FACIRC_1:14;
hence Result s = Following s by A1, A2, Def4; :: thesis: verum