consider p being natural-valued FinSeqLen of 0 ;
consider f being Function of (0 -tuples_on X),X;
take 1GateCircStr p,f ; :: thesis: 1GateCircStr p,f is with_nonpair_inputs
thus 1GateCircStr p,f is with_nonpair_inputs ; :: thesis: verum