let x, y be set ; :: 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 FUNCT_4:87;
for a, b being set holds
( [a,b] in R iff [a,b] in x .--> y )

proof

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

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

assume [a,b] in R ; :: thesis: [a,b] in x .--> y
then ( a in dom R & b in rng R ) by RELAT_1:20;
then ( a = x & b = y ) by A1, A2, TARSKI:def 1;
hence [a,b] in x .--> y by A3, TARSKI:def 1; :: thesis: verum

end;

assume [a,b] in x .--> y ; :: thesis: [a,b] in R
then [a,b] = [x,y] by A3, TARSKI:def 1;
then A4: ( a = x & b = y ) by ZFMISC_1:33;
then a in dom R by A1, TARSKI:def 1;
then consider z being set such that
A5: [a,z] in R by RELAT_1:def 4;
z in rng R by A5, RELAT_1:20;
hence [a,b] in R by A2, A4, A5, TARSKI:def 1; :: thesis: verum

end;

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