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 A3, YELLOW_1:def 4;

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

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 A3, YELLOW_1:def 4;

hereby :: thesis: ( f <= g implies x <= y )

assume A9:
for j being set st j in X holds assume A6:
x <= y
; :: thesis: f <= g

thus f <= g :: thesis: verum

end;thus f <= g :: thesis: verum

proof

let i be set ; :: according to YELLOW_2:def 1 :: thesis: ( not i in X or ex b_{1}, b_{2} being Element of the carrier of L st

( b_{1} = f . i & b_{2} = g . i & b_{1} <= b_{2} ) )

assume A7: i in X ; :: thesis: ex b_{1}, b_{2} being Element of the carrier of L st

( b_{1} = f . i & b_{2} = g . i & b_{1} <= b_{2} )

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_{1}, b_{2} being Element of the carrier of L st

( b_{1} = f . i & b_{2} = g . i & b_{1} <= b_{2} )
by A8; :: thesis: verum

end;( b

assume A7: i in X ; :: thesis: ex b

( b

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

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 ) ) )

hence
x <= y
by A4, A3, YELLOW_1:def 4; :: thesis: verum( 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 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: verum

end;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 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: verum