consider f being Function of (1 -tuples_on X),X;
consider p being FinSeqLen of ;
take 1GateCircStr p,f ; :: thesis: ex A being Circuit of 1GateCircStr p,f st
( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den )
set A = 1GateCircuit p,f;
the Sorts of (1GateCircuit p,f) = the carrier of (1GateCircStr p,f) --> X by CIRCCOMB:def 14;
then ( the Sorts of (1GateCircuit p,f) is constant & the_value_of the Sorts of (1GateCircuit p,f) = X ) by FUNCOP_1:94;
hence ex A being Circuit of 1GateCircStr p,f st
( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den ) ; :: thesis: verum