theorem :: FACIRC_1:23

for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds S1 +* S2 = S2 +* S1 by CIRCCOMB:5, CIRCCOMB:47;