theorem Th5: :: FTACELL2:5

for n being Nat
for ap, bp, cp, dp being FinSequence holds n -BitFTA0Str (ap,bp,cp,dp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (n -BitFTA0Layer2Str (ap,bp,cp,dp))