assume {} in rng (Carrier J) ; :: according to RELAT_1:def 9 :: thesis: contradiction
then consider i being object such that
A1: i in dom (Carrier J) and
A2: (Carrier J) . i = {} by FUNCT_1:def 3;
A3: i in I by A1;
then consider R being 1-sorted such that
A4: R = J . i and
A5: (Carrier J) . i = the carrier of R by PRALG_1:def 15;
A6: R is empty by A2, A5;
i in dom J by A3, PARTFUN1:def 2;
then R in rng J by A4, FUNCT_1:def 3;
hence contradiction by A6, Def2; :: thesis: verum