theorem :: FACIRC_1:9

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
InputVertices (S1 +* S2) is without_pairs by Th8, CIRCCOMB:47;