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