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 consider X being non empty finite set , n being Element of NAT , p being FinSeqLen of , f being Function of (n -tuples_on X),X such that
A2: ( S = 1GateCircStr p,f & A = 1GateCircuit p,f ) by Def7;
reconsider S1 = S as one-gate ManySortedSign by A2;
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 Th20;
hence Following s,1 is stable by FACIRC_1:14; :: thesis: verum