theorem Th6: :: FTACELL2:6

for n being Nat
for ap, bp, cp, dp being FinSequence holds n -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Layer1Circ (ap,bp,cp)) +* (n -BitFTA0Layer2Circ (ap,bp,cp,dp))