let n be Nat; :: thesis: for f being Function of (n -tuples_on BOOLEAN ),BOOLEAN
for p being FinSeqLen of n holds 1GateCircuit p,f is Boolean
let f be Function of (n -tuples_on BOOLEAN ),BOOLEAN ; :: thesis: for p being FinSeqLen of n holds 1GateCircuit p,f is Boolean
let p be FinSeqLen of n; :: thesis: 1GateCircuit p,f is Boolean
set S = 1GateCircStr p,f;
set A = 1GateCircuit p,f;
let v be Vertex of (1GateCircStr p,f); :: according to CIRCCOMB:def 15 :: thesis: the Sorts of (1GateCircuit p,f) . v = BOOLEAN
the Sorts of (1GateCircuit p,f) = the carrier of (1GateCircStr p,f) --> BOOLEAN by Def14;
hence the Sorts of (1GateCircuit p,f) . v = BOOLEAN by FUNCOP_1:13; :: thesis: verum