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 14 :: thesis: the Sorts of (1GateCircuit (p,f)) . v = BOOLEAN
the Sorts of (1GateCircuit (p,f)) = the carrier of (1GateCircStr (p,f)) --> BOOLEAN by Def13;
hence the Sorts of (1GateCircuit (p,f)) . v = BOOLEAN ; :: thesis: verum