theorem Th7: :: FTACELL2:7

for n being Nat
for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) misses InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))