let f be set ; :: thesis: for p being nonpair-yielding FinSequence holds InputVertices (1GateCircStr (p,f)) is without_pairs
let p be nonpair-yielding FinSequence; :: thesis: InputVertices (1GateCircStr (p,f)) is without_pairs
InputVertices (1GateCircStr (p,f)) = rng p by CIRCCOMB:42;
hence InputVertices (1GateCircStr (p,f)) is without_pairs ; :: thesis: verum