let x, X, Y be set ; :: thesis: for f being Function st dom f = {x} & x in X & f . x in Y holds
f is PartFunc of X,Y
let f be Function; :: thesis: ( dom f = {x} & x in X & f . x in Y implies f is PartFunc of X,Y )
assume that
A1: dom f = {x} and
A2: ( x in X & f . x in Y ) ; :: thesis: f is PartFunc of X,Y
rng f = {(f . x)} by A1, FUNCT_1:14;
then ( dom f c= X & rng f c= Y ) by A1, A2, ZFMISC_1:37;
hence f is PartFunc of X,Y by RELSET_1:11; :: thesis: verum