theorem :: GFACIRC2:27

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