assume {} in rng (Carrier J) ; :: thesis: contradiction
then consider i being object such that
A2: i in dom (Carrier J) and
A3: {} = (Carrier J) . i by FUNCT_1:def 3;
A4: dom (Carrier J) = I by PARTFUN1:def 2;
A5: dom J = I by PARTFUN1:def 2;
consider R being 1-sorted such that
A6: R = J . i and
A7: {} = the carrier of R by A2, A3, A4, PRALG_1:def 15;
R in rng J by A2, A4, A5, A6, FUNCT_1:def 3;
then reconsider R = R as non empty RelStr by Def7, YELLOW_1:def 3;
the carrier of R = {} by A7;
hence contradiction ; :: thesis: verum