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