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