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