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