let x be object ; :: thesis: for Y being set
for f being PartFunc of {x},Y holds rng f c= {(f . x)}
let Y be set ; :: thesis: for f being PartFunc of {x},Y holds rng f c= {(f . x)}
let f be PartFunc of {x},Y; :: thesis: rng f c= {(f . x)}
( dom f = {} or dom f = {x} ) by ZFMISC_1:33;
hence rng f c= {(f . x)} by FUNCT_1:4, RELAT_1:42; :: thesis: verum