per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: Y |^ X is reflexive

hence Y |^ X is reflexive by Th26; :: thesis: verum

end;

suppose not X is empty ; :: thesis: Y |^ X is reflexive

then reconsider X = X as non empty set ;
for x being Element of (Y |^ X) holds x <= x

proof

let x be Element of (Y |^ X); :: thesis: x <= x
reconsider x1 = x as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Element of (product (X --> Y)) ;
A1: ex f, g being Function st
( f = x9 & g = x9 & ( 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 ) ) )

proof

take x1 ; :: thesis: ex g being Function st
( x1 = x9 & g = x9 & ( 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 = x1 . i & yi = g . i & xi <= yi ) ) )
take x1 ; :: thesis: ( x1 = x9 & x1 = x9 & ( 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 = x1 . i & yi = x1 . i & xi <= yi ) ) )
thus ( x1 = x9 & x1 = x9 ) ; :: 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 = x1 . i & yi = x1 . 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 = x1 . i & yi = x1 . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
then reconsider i = i as Element of X ;
take R = (X --> Y) . i; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
reconsider xi = x1 . i, yi = x1 . i as Element of R ;
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi )
reconsider xi1 = xi, yi1 = xi as Element of Y ;
xi1 <= yi1 ;
hence ( R = (X --> Y) . i & xi = x1 . i & yi = x1 . i & xi <= yi ) ; :: thesis: verum

end;

x in the carrier of (product (X --> Y)) ;
then x9 in product (Carrier (X --> Y)) by Def4;
hence x <= x by A1, Def4; :: thesis: verum

end;

hence Y |^ X is reflexive by YELLOW_0:def 1; :: thesis: verum

end;

end;