let x be set ; :: thesis: for f being Function holds f . x c= Union f
let f be Function; :: thesis: f . x c= Union f
( x in dom f or not x in dom f ) ;
then ( f . x in rng f or f . x = {} ) by FUNCT_1:3, FUNCT_1:def 2;
hence f . x c= Union f by ZFMISC_1:74; :: thesis: verum