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 n 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 n 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 n holds 1GateCircuit (p,f) is Circuit of X, 1GateCircStr (p,f)
let p be FinSeqLen of n; :: 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 13;
hence ( the Sorts of (1GateCircuit (p,f)) is constant & the_value_of the Sorts of (1GateCircuit (p,f)) = X ) by FUNCOP_1:79; :: thesis: verum