A1: the carrier of (product J) = product (Carrier J) by Def3;

now

assume {} in rng (Carrier J) ; :: thesis: contradiction
then consider i being set such that
A2: ( i in dom (Carrier J) & {} = (Carrier J) . i ) by FUNCT_1:def 5;
A3: ( dom (Carrier J) = I & dom J = I ) by PARTFUN1:def 4;
then consider R being 1-sorted such that
A4: ( R = J . i & {} = the carrier of R ) by A2, PRALG_1:def 13;
R in rng J by A2, A3, A4, FUNCT_1:def 5;
then reconsider R = R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A4;
hence contradiction ; :: thesis: verum

end;

then the carrier of (product J) <> {} by A1, CARD_3:37;
hence not product J is empty ; :: thesis: verum