let f be one-to-one Function; :: thesis: for y being object st rng f = {y} holds
ex x being object st f = x .--> y
let y be object ; :: thesis: ( rng f = {y} implies ex x being object st f = x .--> y )
assume A1: rng f = {y} ; :: thesis: ex x being object st f = x .--> y
then y in rng f by TARSKI:def 1;
then consider x being object such that
A2: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
take x ; :: thesis: f = x .--> y
f is constant by A1;
then dom f = {x} by A2, ZFMISC_1:132;
hence f = x .--> y by A1, FUNCT_4:112; :: thesis: verum