A1: ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) by PRALG_1:def 15;
A2: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
dom (Carrier J) = I by PARTFUN1:def 2;
hence x . i is Element of (J . i) by A1, A2, CARD_3:9; :: thesis: verum