let I be non empty set ; :: thesis: for J, K being RelStr-yielding non-Empty ManySortedSet of 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 ; :: 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: the carrier of (product K) = product (Carrier K) by YELLOW_1:def 4;
A3: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;
A4: ( dom (Carrier J) = I & dom (Carrier K) = I ) by PARTFUN1:def 4;

now

let i be set ; :: 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 ;
A5: ( ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) & ex R being 1-sorted st
( R = K . j & (Carrier K) . j = the carrier of R ) ) by PRALG_1:def 13;
K . j is SubRelStr of J . j by A1;
hence (Carrier K) . i c= (Carrier J) . i by A5, YELLOW_0:def 13; :: thesis: verum

end;

hence A6: the carrier of (product K) c= the carrier of (product J) by A2, A3, A4, CARD_3:38; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of (product K) c= the InternalRel of (product J)
let x, y be set ; :: 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 A7: [x,y] in the InternalRel of (product K) ; :: thesis: [x,y] in the InternalRel of (product J)
then A8: ( x in the carrier of (product K) & y in the carrier of (product K) ) by ZFMISC_1:106;
reconsider x = x, y = y as Element of (product K) by A7, ZFMISC_1:106;
reconsider f = x, g = y as Element of (product J) by A6, A8;
A9: x <= y by A7, ORDERS_2:def 9;

now

let i be Element of I; :: thesis: f . i <= g . i
( K . i is SubRelStr of J . i & x . i <= y . i ) by A1, A9, WAYBEL_3:28;
hence f . i <= g . i by YELLOW_0:60; :: thesis: verum

end;

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