consider A2 being Circuit of S2 such that
A1: ( the Sorts of A2 is constant & the_value_of the Sorts of A2 = X & A2 is gate`2=den ) by Def9;
reconsider A2 = A2 as Circuit of X,S2 by A1, Def10;
consider A1 being Circuit of S1 such that
A2: ( the Sorts of A1 is constant & the_value_of the Sorts of A1 = X & A1 is gate`2=den ) by Def9;
reconsider A1 = A1 as Circuit of X,S1 by A2, Def10;
reconsider A = A1 +* A2 as Circuit of S1 +* S2 by Th28;
S1 +* S2 is Signature of X

proof

take A ; :: according to CIRCCMB3:def 9 :: thesis: ( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den )
thus ( the Sorts of A is constant & the_value_of the Sorts of A = X ) by Th30; :: thesis: A is gate`2=den
thus A is gate`2=den by Th29; :: thesis: verum

end;

hence S1 +* S2 is strict Signature of X ; :: thesis: verum