reconsider z = 0 as Element of NAT ;
set p = the natural-valued FinSeqLen of z;
set f = the Function of (z -tuples_on X),X;
take 1GateCircStr ( the natural-valued FinSeqLen of z, the Function of (z -tuples_on X),X) ; :: thesis: 1GateCircStr ( the natural-valued FinSeqLen of z, the Function of (z -tuples_on X),X) is with_nonpair_inputs
thus 1GateCircStr ( the natural-valued FinSeqLen of z, the Function of (z -tuples_on X),X) is with_nonpair_inputs ; :: thesis: verum