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;
the carrier' of S = {[p,f]} by A1, CIRCCOMB:def 6;
hence Output S is pair by ZFMISC_1:25; :: thesis: verum