let x, y be object ; :: thesis: ( dom {[x,y]} = {x} & rng {[x,y]} = {y} )
set R = {[x,y]};
for z being object holds
( z in dom {[x,y]} iff z in {x} )

proof

let z be object ; :: thesis: ( z in dom {[x,y]} iff z in {x} )
thus ( z in dom {[x,y]} implies z in {x} ) :: thesis: ( z in {x} implies z in dom {[x,y]} )

proof

assume z in dom {[x,y]} ; :: thesis: z in {x}
then consider b being object such that
A2: [z,b] in {[x,y]} by XTUPLE_0:def 12;
[z,b] = [x,y] by A2, TARSKI:def 1;
then z = x by XTUPLE_0:1;
hence z in {x} by TARSKI:def 1; :: thesis: verum

end;

assume z in {x} ; :: thesis: z in dom {[x,y]}
then z = x by TARSKI:def 1;
then [z,y] in {[x,y]} by TARSKI:def 1;
hence z in dom {[x,y]} by XTUPLE_0:def 12; :: thesis: verum

end;

hence dom {[x,y]} = {x} by TARSKI:2; :: thesis: rng {[x,y]} = {y}
for z being object holds
( z in rng {[x,y]} iff z in {y} )

proof

let z be object ; :: thesis: ( z in rng {[x,y]} iff z in {y} )
thus ( z in rng {[x,y]} implies z in {y} ) :: thesis: ( z in {y} implies z in rng {[x,y]} )

proof

assume z in rng {[x,y]} ; :: thesis: z in {y}
then consider a being object such that
A3: [a,z] in {[x,y]} by XTUPLE_0:def 13;
[a,z] = [x,y] by A3, TARSKI:def 1;
then z = y by XTUPLE_0:1;
hence z in {y} by TARSKI:def 1; :: thesis: verum

end;

assume z in {y} ; :: thesis: z in rng {[x,y]}
then z = y by TARSKI:def 1;
then [x,z] in {[x,y]} by TARSKI:def 1;
hence z in rng {[x,y]} by XTUPLE_0:def 13; :: thesis: verum

end;

hence rng {[x,y]} = {y} by TARSKI:2; :: thesis: verum