consider p being FinSeqLen of 1;
consider f being Function of (1 -tuples_on X),X;
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;
A1: the Sorts of (1GateCircuit p,f) = the carrier of (1GateCircStr p,f) --> X by CIRCCOMB:def 14;
then 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 ) by A1; :: thesis: verum