set Y = the carrier of (product J);
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
A2: dom (Carrier J) = I by PARTFUN1:def 2;
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:16;
then A3: pi (X,i) c= pi ( the carrier of (product J),i) by XBOOLE_1:7;
ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) by PRALG_1:def 15;
hence pi (X,i) is Subset of (J . i) by A1, A2, A3, CARD_3:12; :: thesis: verum