set IT = Y |^ X;

now

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)) ;
( x1 in the carrier of (product (X --> Y)) & y1 in the carrier of (product (X --> Y)) ) ;
then A1: ( x1 in product (Carrier (X --> Y)) & y1 in product (Carrier (X --> Y)) ) by Def4;
assume A2: ( x <= y & y <= z ) ; :: thesis: x <= z
then consider f, g being Function such that
A3: ( f = x1 & g = y1 & ( for i being set 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;
consider f1, g1 being Function such that
A4: ( f1 = y1 & g1 = z1 & ( for i being set 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 A1, A2, Def4;
ex f2, g2 being Function st
( f2 = x1 & g2 = z1 & ( for i being set 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 set 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 set 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 set 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 set ; :: 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 A5: 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 A5;
reconsider R = (X --> Y) . i as RelStr ;
A6: R = Y by FUNCOP_1:13;
then reconsider xi = f2 . i, yi = g2 . i as Element of R by FUNCT_2:7;
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 )
consider R1 being RelStr , xi1, yi1 being Element of R1 such that
A7: ( R1 = (X --> Y) . i & xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) by A3;
consider R2 being RelStr , xi2, yi2 being Element of R2 such that
A8: ( R2 = (X --> Y) . i & xi2 = f1 . i & yi2 = g1 . i & xi2 <= yi2 ) by A4;
thus ( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) by A3, A4, A6, A7, A8, YELLOW_0:def 2; :: thesis: verum

end;

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

end;

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