let X be set ; :: thesis: for x being object
for f being X -valued Function st x in dom f holds
f . x is Element of X
let x be object ; :: thesis: for f being X -valued Function st x in dom f holds
f . x is Element of X
let f be X -valued Function; :: thesis: ( x in dom f implies f . x is Element of X )
assume x in dom f ; :: thesis: f . x is Element of X
then A1: f . x in rng f by Def3;
rng f c= X by RELAT_1:def 19;
hence f . x is Element of X by A1; :: thesis: verum