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