consider f being Function of 1 -tuples_on X,X;
consider p being FinSeqLen of 1;
1GateCircStr p,f is Signature of X by Th27;
hence ex b₁ being Signature of X st
( b₁ is strict & b₁ is one-gate ) ; :: thesis: verum