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;

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 b₁, b₂ being Element of the carrier of L st
( b₁ = f . i & b₂ = g . i & b₁ <= b₂ ) )
assume A7: i in X ; :: thesis: ex b₁, b₂ being Element of the carrier of L st
( b₁ = f . i & b₂ = g . i & 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₂ being Element of the carrier of L st
( b₁ = f . i & b₂ = g . i & b₁ <= b₂ ) 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 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;

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