let x be set ; :: thesis: for f being Function holds
( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) )
let f be Function; :: thesis: ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) )
( ( x in f " (SubFuncs (rng f)) implies ( x in dom f & f . x in SubFuncs (rng f) ) ) & ( x in dom f & f . x in SubFuncs (rng f) implies x in f " (SubFuncs (rng f)) ) & ( f . x in rng f & f . x is Function implies f . x in SubFuncs (rng f) ) & ( f . x in SubFuncs (rng f) implies ( f . x in rng f & f . x is Function ) ) & ( x in dom f implies f . x in rng f ) ) by Def1, FUNCT_1:def 5, FUNCT_1:def 13;
hence ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) ) ; :: thesis: verum