let X be set ; :: thesis:
let L be non empty RelStr ; :: thesis:
let f, g be Function of X, the carrier of L; :: thesis:
let x, y be Element of (L |^ X); :: thesis:
assume that
A1: x = f and
A2: y = g ; :: thesis:
set J = X --> L;
A3: L |^ X = product (X --> L) by YELLOW_1:def 5;
A4: the carrier of (product (X --> L)) = product (Carrier (X --> L)) by YELLOW_1:def 4;
then A5: ( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) by A3, YELLOW_1:def 4;

let i be set ; :: according to YELLOW_2:def 1 :: thesis:
assume A7: i in X ; :: thesis:
then A8: (X --> L) . i = L by FUNCOP_1:7;
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f . i & yi = g . i & xi <= yi ) by A1, A2, A5, A6, A7;
hence ex b₁, b₂ being Element of the carrier of L st
( b₁ = f . i & b₂ = g . i & b₁ <= b₂ ) by A8; :: thesis:

end;

assume A9: for j being set st j in X holds
ex a, b being Element of L st
( a = f . j & b = g . j & a <= b ) ; :: according to YELLOW_2:def 1 :: thesis:

reconsider f9 = f, g9 = g as Function ;
take f9 = f9; :: thesis:
take g9 = g9; :: thesis:
thus ( f9 = x & g9 = y ) by A1, A2; :: thesis:
let i be object ; :: thesis:
assume A10: i in X ; :: thesis:
then A11: (X --> L) . i = L by FUNCOP_1:7;
ex a, b being Element of L st
( a = f . i & b = g . i & a <= b ) by A9, A10;
hence ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) by A11; :: thesis:

end;