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 A1: ( x = f & y = g ) ; :: thesis: ( x <= y iff f <= g )
set J = X --> L;
A2: ( the carrier of (product (X --> L)) <> {} & the carrier of (product (X --> L)) = product (Carrier (X --> L)) & L |^ X = product (X --> L) ) by YELLOW_1:def 4, YELLOW_1:def 5;
then A3: ( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being set 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 YELLOW_1:def 4;

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

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

end;

end;

assume A5: 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

reconsider f' = f, g' = g as Function ;
take f' = f'; :: thesis: ex g' being Function st
( f' = x & g' = y & ( for i being set 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 ) ) )
take g' = g'; :: thesis: ( f' = x & g' = y & ( for i being set 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 ) ) )
thus ( f' = x & g' = y ) by A1; :: thesis: for i being set 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 )
let i be set ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f' . i & yi = g' . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f' . i & yi = g' . i & xi <= yi )
then ( (X --> L) . i = L & ex a, b being Element of L st
( a = f . i & b = g . i & a <= b ) ) by A5, FUNCOP_1:13;
hence ex R being RelStr ex xi, yi being Element of R st
( R = (X --> L) . i & xi = f' . i & yi = g' . i & xi <= yi ) ; :: thesis: verum

end;

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