let S be one-gate ManySortedSign ; :: thesis: InnerVertices S = {(Output S)}
consider X being non empty finite set , n being Element of NAT , p being FinSeqLen of n, f being Function of (n -tuples_on X),X such that
A1: S = 1GateCircStr (p,f) by Def6;
Output S = [p,f] by A1, Th15;
hence InnerVertices S = {(Output S)} by A1, CIRCCOMB:42; :: thesis: verum