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 1GateCircStr (p,f) is Signature of X
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 1GateCircStr (p,f) is Signature of X
let f be Function of (n -tuples_on X),X; :: thesis: for p being FinSeqLen of n holds 1GateCircStr (p,f) is Signature of X
let p be FinSeqLen of n; :: thesis: 1GateCircStr (p,f) is Signature of X
take A = 1GateCircuit (p,f); :: according to CIRCCMB3:def 9 :: thesis: ( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den )
the Sorts of A = the carrier of (1GateCircStr (p,f)) --> X by CIRCCOMB:def 13;
hence ( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den ) by FUNCOP_1:79; :: thesis: verum