consider n being Element of NAT , X being non empty finite set ;
consider f being Function of n -tuples_on X,X;
consider p being natural-valued FinSeqLen of n;
take 1GateCircStr p,f ; :: thesis: 1GateCircStr p,f is with_nonpair_inputs
thus 1GateCircStr p,f is with_nonpair_inputs ; :: thesis: verum