let Y, x be set ; :: thesis: for f being Y -valued Function st x in dom f holds
f . x in Y
let f be Y -valued Function; :: 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, RELAT_1:def 19;
hence f . x in Y ; :: thesis: verum