the carrier of (1GateCircStr (p,x)) = (rng p) \/ {[p,x]} by CIRCCOMB:def 6;
hence 1GateCircStr (p,x) is finite ; :: thesis: verum