the Sorts of A1 tolerates the Sorts of A2 by Th67;
hence ( A1 +* A2 is Boolean & A1 +* A2 is gate`2=den ) by Th70, Th71; :: thesis: verum