dom A = J by PARTFUN1:def 2;
hence A . j is Universal_Algebra by Def10; :: thesis: verum