consider X being non empty finite set , n being Element of NAT , p being FinSeqLen of , f being Function of (n -tuples_on X),X such that
A1: S = 1GateCircStr p,f by Def6;
reconsider A = 1GateCircuit p,f as finite-yielding MSAlgebra of S by A1;
take A ; :: thesis: ( A is one-gate & A is non-empty )
thus ( A is one-gate & A is non-empty ) by A1; :: thesis: verum