let I be non empty set ; :: thesis: for J, K being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds K . i is SubRelStr of J . i ) holds
product K is SubRelStr of product J
let J, K be RelStr-yielding non-Empty ManySortedSet of I; :: thesis: ( ( for i being Element of I holds K . i is SubRelStr of J . i ) implies product K is SubRelStr of product J )
assume A1: for i being Element of I holds K . i is SubRelStr of J . i ; :: thesis: product K is SubRelStr of product J

A2: now :: thesis: for i being object st i in I holds
(Carrier K) . i c= (Carrier J) . i

let i be object ; :: thesis: ( i in I implies (Carrier K) . i c= (Carrier J) . i )
assume i in I ; :: thesis: (Carrier K) . i c= (Carrier J) . i
then reconsider j = i as Element of I ;
A3: ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) by PRALG_1:def 15;
A4: ex R being 1-sorted st
( R = K . j & (Carrier K) . j = the carrier of R ) by PRALG_1:def 15;
K . j is SubRelStr of J . j by A1;
hence (Carrier K) . i c= (Carrier J) . i by A3, A4, YELLOW_0:def 13; :: thesis: verum

end;

A5: dom (Carrier K) = I by PARTFUN1:def 2;
A6: dom (Carrier J) = I by PARTFUN1:def 2;
A7: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
the carrier of (product K) = product (Carrier K) by YELLOW_1:def 4;
hence A8: the carrier of (product K) c= the carrier of (product J) by A7, A6, A5, A2, CARD_3:27; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of (product K) c= the InternalRel of (product J)
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of (product K) or [x,y] in the InternalRel of (product J) )
assume A9: [x,y] in the InternalRel of (product K) ; :: thesis: [x,y] in the InternalRel of (product J)
reconsider x = x, y = y as Element of (product K) by A9, ZFMISC_1:87;
reconsider f = x, g = y as Element of (product J) by A8;
A10: x <= y by A9, ORDERS_2:def 5;

now :: thesis: for i being Element of I holds f . i <= g . i

let i be Element of I; :: thesis: f . i <= g . i
A11: x . i <= y . i by A10, WAYBEL_3:28;
K . i is SubRelStr of J . i by A1;
hence f . i <= g . i by A11, YELLOW_0:59; :: thesis: verum

end;

then f <= g by WAYBEL_3:28;
hence [x,y] in the InternalRel of (product J) by ORDERS_2:def 5; :: thesis: verum