dom A = J by PBOOLE:def 3;
hence A . j is 1-sorted by Def11; :: thesis: verum