let A be Circuit of X,S; :: thesis: ( A is gate`2=den & A is non-empty )
thus A is gate`2=den by Def10; :: thesis: A is non-empty
( not the Sorts of A is empty & the Sorts of A is constant & the_value_of the Sorts of A = X ) by Def10;
then ( dom the Sorts of A = the carrier of S & ( for i being object st i in dom the Sorts of A holds
not the Sorts of A . i is empty ) ) by FUNCT_1:def 12, PARTFUN1:def 2;
then the Sorts of A is V8() by PBOOLE:def 13;
hence A is non-empty by MSUALG_1:def 3; :: thesis: verum