let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not (Carrier F) . i is empty )
assume A1: i in I ; :: thesis: not (Carrier F) . i is empty
then A2: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def 13;
dom F = I by PARTFUN1:def 4;
then F . i in rng F by A1, FUNCT_1:def 5;
then F . i is non empty multMagma by Def1;
hence not (Carrier F) . i is empty by A2; :: thesis: verum