let X be set ; 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 ; 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; 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); ( x = f & y = g implies ( x <= y iff f <= g ) )
assume that
A1:
x = f
and
A2:
y = g
; ( 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 ( f <= g implies x <= y )
assume A6:
x <= y
;
f <= gthus
f <= g
verum
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 )
; YELLOW_2:def 1 x <= y
now 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;
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;
( 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;
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 ;
( 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
;
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;
verum end;
hence
x <= y
by A4, A3, YELLOW_1:def 4; verum