A1: ( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X ) by Th30;
( A1 +* A2 is gate`2=den & A1 +* A2 is Circuit of S1 +* S2 ) by Th28, Th29;
hence A1 +* A2 is strict Circuit of X,S1 +* S2 by A1, Def10; :: thesis: verum