dom A = J by PARTFUN1:def 2;
then A . j in rng A by FUNCT_1:def 3;
hence A . j is TopStruct by Def1; :: thesis: verum