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 , f being Function of (n -tuples_on X),X such that
A1: S = 1GateCircStr p,f by Def6;
Output S = [p,f] by A1, Th16;
hence InnerVertices S = {(Output S)} by A1, CIRCCOMB:49; :: thesis: verum