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