let A be non-empty Circuit of S; :: thesis: ( A is one-gate implies A is with_stabilization-limit )
assume A1: A is one-gate ; :: thesis: A is with_stabilization-limit
then ex X being non empty finite set ex n being Element of NAT ex p being FinSeqLen of n ex f being Function of (n -tuples_on X),X st
( S = 1GateCircStr (p,f) & A = 1GateCircuit (p,f) ) ;
then reconsider S1 = S as one-gate ManySortedSign ;
reconsider A1 = A as one-gate Circuit of S1 by A1;
take 1 ; :: according to CIRCCMB3:def 3 :: thesis: for s being State of A holds Following (s,1) is stable
let s be State of A; :: thesis: Following (s,1) is stable
reconsider s1 = s as State of A1 ;
Following s1 is stable by Th19;
hence Following (s,1) is stable by FACIRC_1:14; :: thesis: verum