let x be object ; :: thesis: for Y being set
for f being b₁ -valued Function st x in dom f holds
f . x in Y
let Y 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 A1: f . x in rng f by FUNCT_1:def 3;
rng f c= Y by RELAT_1:def 19;
hence f . x in Y by A1; :: thesis: verum