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 Th38;
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: K45(the InternalRel of (product J),the carrier of S) c= the InternalRel of S
let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in K45(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:106;
reconsider a = x, b = y as Element of (product J) by YELLOW_0:59;
reconsider x = x, y = y as Element of (product K) ;
A5: a <= b by A4, ORDERS_2:def 9;

now

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:61; :: thesis: verum

end;

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

end;

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