let n be Element of NAT ; :: thesis: for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of holds 1GateCircuit p,f is Circuit of X, 1GateCircStr p,f
let X be non empty finite set ; :: thesis: for f being Function of (n -tuples_on X),X
for p being FinSeqLen of holds 1GateCircuit p,f is Circuit of X, 1GateCircStr p,f
let f be Function of (n -tuples_on X),X; :: thesis: for p being FinSeqLen of holds 1GateCircuit p,f is Circuit of X, 1GateCircStr p,f
let p be FinSeqLen of ; :: thesis: 1GateCircuit p,f is Circuit of X, 1GateCircStr p,f
set A = 1GateCircuit p,f;
thus 1GateCircuit p,f is gate`2=den ; :: according to CIRCCMB3:def 10 :: thesis: ( the Sorts of (1GateCircuit p,f) is constant & the_value_of the Sorts of (1GateCircuit p,f) = X )
the Sorts of (1GateCircuit p,f) = the carrier of (1GateCircStr p,f) --> X by CIRCCOMB:def 14;
hence ( the Sorts of (1GateCircuit p,f) is constant & the_value_of the Sorts of (1GateCircuit p,f) = X ) by FUNCOP_1:94; :: thesis: verum