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;
take 1GateCircStr p,f ; :: thesis: 1GateCircStr p,f is one-gate
thus 1GateCircStr p,f is one-gate ; :: thesis: verum