set X = the non empty finite set ;
set n = the Element of NAT ;
set p = the FinSeqLen of the Element of NAT ;
set f = the Function of ( the Element of NAT -tuples_on the non empty finite set ), the non empty finite set ;
take 1GateCircStr ( the 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 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 one-gate
thus 1GateCircStr ( the 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 one-gate ; :: thesis: verum