consider p being FinSeqLen of 1;
consider f being Function of (1 -tuples_on X),X;
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