set IT = Y |^ X;

now :: thesis: for x, y, z being Element of (Y |^ X) st x <= y & y <= z holds
x <= z

let x, y, z be Element of (Y |^ X); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi )
take yi ; :: thesis: ( 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; :: thesis: verum

end;

hence x <= z by A5, Def4; :: thesis: verum

end;

hence Y |^ X is transitive by YELLOW_0:def 2; :: thesis: verum