let x be object ; :: thesis: for X, Y being set
for f being Function st dom f = {x} & x in X & f . x in Y holds
f is PartFunc of X,Y
let 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 and
A3: f . x in Y ; :: thesis: f is PartFunc of X,Y
rng f = {(f . x)} by A1, FUNCT_1:4;
then A4: rng f c= Y by A3, ZFMISC_1:31;
dom f c= X by A1, A2, ZFMISC_1:31;
hence f is PartFunc of X,Y by A4, RELSET_1:4; :: thesis: verum