let S be ManySortedSign ; :: thesis: ( S is one-gate implies ( S is strict & not S is void & not S is empty & S is unsplit & S is gate`1=arity & S is finite ) )
assume S is one-gate ; :: thesis: ( S is strict & not S is void & not S is empty & S is unsplit & S is gate`1=arity & S is finite )
then ex X being non empty finite set ex n being Element of NAT ex p being FinSeqLen of n ex f being Function of (n -tuples_on X),X st S = 1GateCircStr (p,f) by Def6;
hence ( S is strict & not S is void & not S is empty & S is unsplit & S is gate`1=arity & S is finite ) ; :: thesis: verum