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;
A1 +* A2 is gate`2=den by Th29;
hence S1 +* S2 is gate`2=den ; :: thesis: verum