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 14;
hence ( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den ) by FUNCOP_1:94; :: thesis: verum