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 full SubRelStr of J . i ) holds
product K is full 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 full SubRelStr of J . i ) implies product K is full SubRelStr of product J )
assume A1: for i being Element of I holds K . i is full SubRelStr of J . i ; :: thesis: product K is full SubRelStr of product J
then for i being Element of I holds K . i is SubRelStr of J . i ;
then reconsider S = product K as non empty SubRelStr of product J by Th35;
A2: the InternalRel of (product J) |_2 the carrier of S = the InternalRel of (product J) /\ [: the carrier of S, the carrier of S:] by WELLORD1:def 6;
S is full

proof

the InternalRel of S c= the InternalRel of (product J) by YELLOW_0:def 13;
hence the InternalRel of S c= the InternalRel of (product J) |_2 the carrier of S by A2, XBOOLE_1:19; :: according to YELLOW_0:def 14,XBOOLE_0:def 10 :: thesis: K44( the InternalRel of (product J), the carrier of S) c= the InternalRel of S
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in K44( the InternalRel of (product J), the carrier of S) or [x,y] in the InternalRel of S )
assume A3: [x,y] in the InternalRel of (product J) |_2 the carrier of S ; :: thesis: [x,y] in the InternalRel of S
then A4: [x,y] in the InternalRel of (product J) by A2, XBOOLE_0:def 4;
[x,y] in [: the carrier of S, the carrier of S:] by A2, A3, XBOOLE_0:def 4;
then reconsider x = x, y = y as Element of S by ZFMISC_1:87;
reconsider a = x, b = y as Element of (product J) by YELLOW_0:58;
reconsider x = x, y = y as Element of (product K) ;
A5: a <= b by A4, ORDERS_2:def 5;

now :: thesis: for i being Element of I holds x . i <= y . i

let i be Element of I; :: thesis: x . i <= y . i
A6: K . i is full SubRelStr of J . i by A1;
a . i <= b . i by A5, WAYBEL_3:28;
hence x . i <= y . i by A6, YELLOW_0:60; :: thesis: verum

end;

then x <= y by WAYBEL_3:28;
hence [x,y] in the InternalRel of S by ORDERS_2:def 5; :: thesis: verum

end;

hence product K is full SubRelStr of product J ; :: thesis: verum