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 finite-yielding MSAlgebra over 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