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