let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in J or not (Carrier A) . i is empty )
A0: dom A = J by PARTFUN1:def 2;
assume A1: i in J ; :: thesis: not (Carrier A) . i is empty
then consider R being 1-sorted such that
A2: R = A . i and
A3: (Carrier A) . i = the carrier of R by Def13, A0;
dom A = J by PARTFUN1:def 2;
then R is Universal_Algebra by A1, A2, Def10;
hence not (Carrier A) . i is empty by A3; :: thesis: verum