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;

hence ex b_{1} being Function of X,Y st b_{1} is E,F -respecting
; :: thesis: verum

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

then
f is E,F -respecting
;[(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;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

hence ex b