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