let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not (Carrier F) . i is empty )

assume A1: i in I ; :: thesis: not (Carrier F) . i is empty

dom F = I by PARTFUN1:def 2;

then F . i in rng F by A1, FUNCT_1:def 3;

then A2: F . i is non empty multMagma by Def1;

ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by A1, PRALG_1:def 15;

hence not (Carrier F) . i is empty by A2; :: thesis: verum

assume A1: i in I ; :: thesis: not (Carrier F) . i is empty

dom F = I by PARTFUN1:def 2;

then F . i in rng F by A1, FUNCT_1:def 3;

then A2: F . i is non empty multMagma by Def1;

ex R being 1-sorted st

( R = F . i & (Carrier F) . i = the carrier of R ) by A1, PRALG_1:def 15;

hence not (Carrier F) . i is empty by A2; :: thesis: verum