let X be set ; :: thesis: for L being non empty RelStr
for f, g being Function of X, the carrier of L
for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )

let L be non empty RelStr ; :: thesis: for f, g being Function of X, the carrier of L
for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )

let f, g be Function of X, the carrier of L; :: thesis: for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )

let x, y be Element of (L |^ X); :: thesis: ( x = f & y = g implies ( x <= y iff f <= g ) )
assume that
A1: x = f and
A2: y = g ; :: thesis: ( x <= y iff f <= g )
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 ;
hereby :: thesis: ( f <= g implies x <= y )
assume A6: x <= y ; :: thesis: f <= g
thus f <= g :: thesis: verum
proof
let i be set ; :: according to YELLOW_2:def 1 :: thesis: ( not i in X or ex b1, b2 being Element of the carrier of L st
( b1 = f . i & b2 = g . i & b1 <= b2 ) )

assume A7: i in X ; :: thesis: ex b1, b2 being Element of the carrier of L st
( b1 = f . i & b2 = g . i & b1 <= b2 )

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 b1, b2 being Element of the carrier of L st
( b1 = f . i & b2 = g . i & b1 <= b2 ) by A8; :: thesis: verum
end;
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: x <= y
now :: thesis: ex f9, g9 being Function st
( f9 = x & g9 = 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 = f9 . i & yi = g9 . i & xi <= yi ) ) )
reconsider f9 = f, g9 = g as Function ;
take f9 = f9; :: thesis: ex g9 being Function st
( f9 = x & g9 = 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 = f9 . i & yi = g9 . i & xi <= yi ) ) )

take g9 = g9; :: thesis: ( f9 = x & g9 = 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 = f9 . i & yi = g9 . i & xi <= yi ) ) )

thus ( f9 = x & g9 = y ) by A1, A2; :: thesis: 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 = f9 . i & yi = g9 . i & xi <= yi )

let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi ) )

assume A10: i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f9 . i & yi = g9 . i & xi <= yi )

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 ;
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: verum
end;
hence x <= y by ; :: thesis: verum