consider X being non empty finite set , n being Element of NAT , p being FinSeqLen of n, f being Function of (n -tuples_on X),X such that
A1: S = 1GateCircStr (p,f) by Def6;
[p,f] in {[p,f]} by TARSKI:def 1;
then A2: [p,f] in (rng p) \/ {[p,f]} by XBOOLE_0:def 3;
the carrier' of S = {[p,f]} by A1, CIRCCOMB:def 6;
then union the carrier' of S = [p,f] by ZFMISC_1:25;
hence union the carrier' of S is Vertex of S by A1, A2, CIRCCOMB:def 6; :: thesis: verum