set Y = the carrier of (product J);
A1: ( the carrier of (product J) = product (Carrier J) & dom (Carrier J) = I ) by PARTFUN1:def 4, YELLOW_1:def 4;
X \/ the carrier of (product J) = the carrier of (product J) by XBOOLE_1:12;
then pi the carrier of (product J),i = (pi X,i) \/ (pi the carrier of (product J),i) by CARD_3:27;
then A2: ( pi X,i c= pi the carrier of (product J),i & pi the carrier of (product J),i = (Carrier J) . i ) by A1, CARD_3:22, XBOOLE_1:7;
ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) by PRALG_1:def 13;
hence pi X,i is Subset of (J . i) by A2; :: thesis: verum