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 ) )
( ( f . x in rng f & f . x is Function ) iff f . x in SubFuncs (rng f) ) by Def1;
hence ( x in f " (SubFuncs (rng f)) iff ( x in dom f & f . x is Function ) ) by FUNCT_1:def 3, FUNCT_1:def 7; :: thesis: verum