let X, Y, x be set ; :: thesis: for f being PartFunc of X,Y st x in dom f holds
f . x in Y
let f be PartFunc of X,Y; :: thesis: ( x in dom f implies f . x in Y )
assume x in dom f ; :: thesis: f . x in Y
then ( f . x in rng f & rng f c= Y ) by FUNCT_1:def 5, RELSET_1:12;
hence f . x in Y ; :: thesis: verum