consider X being non empty finite set , n being Element of NAT , p being FinSeqLen of n, f being Function of n -tuples_on X,X such that
A1: S = 1GateCircStr p,f by Def6;
reconsider A = 1GateCircuit p,f as locally-finite 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