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