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