let A, B be non empty set ; :: thesis: for x being Element of A
for f being Function of A,B holds f . x in rng f
let x be Element of A; :: thesis: for f being Function of A,B holds f . x in rng f
let f be Function of A,B; :: thesis: f . x in rng f
dom f = A by Def1;
hence f . x in rng f by FUNCT_1:def 3; :: thesis: verum