dom A = I by PARTFUN1:def 4;
then A . j in rng A by FUNCT_1:def 5;
hence A . j is TopStruct by Def13; :: thesis: verum