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