theorem Th16: :: FTACELL2:16

for n being Nat
for ap, bm, cp, dm being FinSequence holds n -BitFTA1Str (ap,bm,cp,dm) = (n -BitFTA1Layer1Str (ap,bm,cp)) +* (n -BitFTA1Layer2Str (ap,bm,cp,dm))