let f be Function; :: thesis: for x, y being set st dom f = {x} & rng f = {y} holds
f = {[x,y]}
let x, y be set ; :: thesis: ( dom f = {x} & rng f = {y} implies f = {[x,y]} )
assume ( dom f = {x} & rng f = {y} ) ; :: thesis: f = {[x,y]}
then f = {x} --> y by FUNCOP_1:9;
hence f = {[x,y]} by ZFMISC_1:29; :: thesis: verum