theorem Th8: :: FTACELL2:8
for n being Nat
for ap, bp, cp being nonpair-yielding FinSequence
for s being State of (n -BitFTA0Layer1Circ (ap,bp,cp)) holds Following (s,2) is stable