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;

now :: thesis: for x1, x2 being set st [x1,x2] in E holds
[(f . x1),(f . x2)] in F

let x1, x2 be set ; :: thesis: ( [x1,x2] in E implies [(f . x1),(f . x2)] in F )
assume [x1,x2] in E ; :: thesis: [(f . x1),(f . x2)] in F
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: verum

end;

then f is E,F -respecting ;
hence ex b₁ being Function of X,Y st b₁ is E,F -respecting ; :: thesis: verum