set IT = Y |^ X;
now for x, y, z being Element of (Y |^ X) st x <= y & y <= z holds
x <= zlet x,
y,
z be
Element of
(Y |^ X);
( x <= y & y <= z implies x <= z )reconsider x1 =
x,
y1 =
y,
z1 =
z as
Element of
(product (X --> Y)) ;
assume that A1:
x <= y
and A2:
y <= z
;
x <= z
y1 in the
carrier of
(product (X --> Y))
;
then
y1 in product (Carrier (X --> Y))
by Def4;
then consider f1,
g1 being
Function such that A3:
(
f1 = y1 &
g1 = z1 )
and A4:
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (X --> Y) . i &
xi = f1 . i &
yi = g1 . i &
xi <= yi )
by A2, Def4;
x1 in the
carrier of
(product (X --> Y))
;
then A5:
x1 in product (Carrier (X --> Y))
by Def4;
then consider f,
g being
Function such that A6:
(
f = x1 &
g = y1 )
and A7:
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (X --> Y) . i &
xi = f . i &
yi = g . i &
xi <= yi )
by A1, Def4;
ex
f2,
g2 being
Function st
(
f2 = x1 &
g2 = z1 & ( for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (X --> Y) . i &
xi = f2 . i &
yi = g2 . i &
xi <= yi ) ) )
proof
reconsider f2 =
x,
g2 =
z as
Function of
X, the
carrier of
Y by Lm5;
take
f2
;
ex g2 being Function st
( f2 = x1 & g2 = z1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )
take
g2
;
( f2 = x1 & g2 = z1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) ) )
thus
(
f2 = x1 &
g2 = z1 )
;
for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . 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 --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) )
assume A8:
i in X
;
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
then reconsider X =
X as non
empty set ;
reconsider i =
i as
Element of
X by A8;
reconsider R =
(X --> Y) . i as
RelStr ;
reconsider xi =
f2 . i,
yi =
g2 . i as
Element of
R by FUNCT_2:5;
take
R
;
ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take
xi
;
ex yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take
yi
;
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
( ex
R1 being
RelStr ex
xi1,
yi1 being
Element of
R1 st
(
R1 = (X --> Y) . i &
xi1 = f . i &
yi1 = g . i &
xi1 <= yi1 ) & ex
R2 being
RelStr ex
xi2,
yi2 being
Element of
R2 st
(
R2 = (X --> Y) . i &
xi2 = f1 . i &
yi2 = g1 . i &
xi2 <= yi2 ) )
by A7, A4;
hence
(
R = (X --> Y) . i &
xi = f2 . i &
yi = g2 . i &
xi <= yi )
by A6, A3, YELLOW_0:def 2;
verum
end; hence
x <= z
by A5, Def4;
verum end;
hence
Y |^ X is transitive
by YELLOW_0:def 2; verum