consider f being Function of 1 -tuples_on X,X;
consider p being FinSeqLen of 1;
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 YELLOW_6:2;
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