dom A = J by PARTFUN1:def 2;
hence A . j is 1-sorted by Def11a; :: thesis: verum