let x, y, a, b be set ; :: thesis: (x,y) --> (a,b) c= [:{x,y},{a,b}:]
set f = (x,y) --> (a,b);

now :: thesis: ( (x,y) --> (a,b) c= [:(dom ((x,y) --> (a,b))),(rng ((x,y) --> (a,b))):] & [:(dom ((x,y) --> (a,b))),(rng ((x,y) --> (a,b))):] c= [:{x,y},{a,b}:] )

thus (x,y) --> (a,b) c= [:(dom ((x,y) --> (a,b))),(rng ((x,y) --> (a,b))):] by RELAT_1:7; :: thesis: [:(dom ((x,y) --> (a,b))),(rng ((x,y) --> (a,b))):] c= [:{x,y},{a,b}:]
( dom ((x,y) --> (a,b)) = {x,y} & rng ((x,y) --> (a,b)) c= {a,b} ) by FUNCT_4:62;
hence [:(dom ((x,y) --> (a,b))),(rng ((x,y) --> (a,b))):] c= [:{x,y},{a,b}:] by ZFMISC_1:96; :: thesis: verum

end;

hence (x,y) --> (a,b) c= [:{x,y},{a,b}:] ; :: thesis: verum