let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty ManySortedSet of I
for x, y being Element of (product J) holds
( x <= y iff for i being Element of I holds x . i <= y . i )
let J be RelStr-yielding non-Empty ManySortedSet of I; :: thesis: for x, y being Element of (product J) holds
( x <= y iff for i being Element of I holds x . i <= y . i )
set L = product J;
let x, y be Element of (product J); :: thesis: ( x <= y iff for i being Element of I holds x . i <= y . i )
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def 4;

hereby :: thesis: ( ( for i being Element of I holds x . i <= y . i ) implies x <= y )

assume A2: x <= y ; :: thesis: for i being Element of I holds x . i <= y . i
let i be Element of I; :: thesis: x . i <= y . i
ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A1, A2, YELLOW_1:def 4;
then ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = y . i & xi <= yi ) ;
hence x . i <= y . i ; :: thesis: verum

end;

assume A3: for i being Element of I holds x . i <= y . i ; :: thesis: x <= y
ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) )

proof

take f = x; :: thesis: ex g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take g = y; :: thesis: ( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) )
thus ( f = x & g = y ) ; :: thesis: for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi )
let i be object ; :: thesis: ( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) )
assume i in I ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi )
then reconsider j = i as Element of I ;
take J . j ; :: thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = f . i & yi = g . i & xi <= yi )
take x . j ; :: thesis: ex yi being Element of (J . j) st
( J . j = J . i & x . j = f . i & yi = g . i & x . j <= yi )
take y . j ; :: thesis: ( J . j = J . i & x . j = f . i & y . j = g . i & x . j <= y . j )
thus ( J . j = J . i & x . j = f . i & y . j = g . i & x . j <= y . j ) by A3; :: thesis: verum

end;

hence x <= y by A1, YELLOW_1:def 4; :: thesis: verum