theorem :: FSCIRC_2:21

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