theorem :: FACIRC_2:27

for n being Nat
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitAdderStr (x,y)) = (rng x) \/ (rng y)