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

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