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