consider y being object such that
A1: y in Y by XBOOLE_0:7;
set R = X --> y;
( {y} c= Y & dom (X --> y) = X & rng (X --> y) c= {y} ) by ZFMISC_1:31, A1;
then reconsider f = X --> y as Function of X,Y by FUNCT_2:2;

let x1, x2 be set ; :: thesis:
assume [x1,x2] in E ; :: thesis:
then ( x1 in X & x2 in X ) by ZFMISC_1:87;
then A2: ( f . x1 = y & f . x2 = y ) by FUNCOP_1:7;
thus [(f . x1),(f . x2)] in F by A2, A1, EQREL_1:5; :: thesis:

end;