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