let y, x be object ; :: thesis: for R being Relation st dom R = {x} & rng R = {y} holds
R = x .--> y
let R be Relation; :: thesis: ( dom R = {x} & rng R = {y} implies R = x .--> y )
assume that
A1: dom R = {x} and
A2: rng R = {y} ; :: thesis: R = x .--> y
set g = x .--> y;
A3: x .--> y = {[x,y]} by ZFMISC_1:29;
for a, b being object holds
( [a,b] in R iff [a,b] in x .--> y )

proof

let a, b be object ; :: thesis: ( [a,b] in R iff [a,b] in x .--> y )

hereby :: thesis: ( [a,b] in x .--> y implies [a,b] in R )

assume A4: [a,b] in R ; :: thesis: [a,b] in x .--> y
then b in rng R by XTUPLE_0:def 13;
then A5: b = y by A2, TARSKI:def 1;
a in dom R by A4, XTUPLE_0:def 12;
then a = x by A1, TARSKI:def 1;
hence [a,b] in x .--> y by A3, A5, TARSKI:def 1; :: thesis: verum

end;

assume [a,b] in x .--> y ; :: thesis: [a,b] in R
then A6: [a,b] = [x,y] by A3, TARSKI:def 1;
then A7: b = y by XTUPLE_0:1;
a = x by A6, XTUPLE_0:1;
then a in dom R by A1, TARSKI:def 1;
then consider z being object such that
A8: [a,z] in R by XTUPLE_0:def 12;
z in rng R by A8, XTUPLE_0:def 13;
hence [a,b] in R by A2, A7, A8, TARSKI:def 1; :: thesis: verum

end;

hence R = x .--> y by RELAT_1:def 2; :: thesis: verum