let x, 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:39;
then ( rng f = {} or rng f = {(f . x)} ) by FUNCT_1:14, RELAT_1:65;
hence rng f c= {(f . x)} by ZFMISC_1:39; :: thesis: verum