let f be Function-yielding Function; :: thesis: SubFuncs (rng f) = rng f
for x being set st x in rng f holds
x is Function

proof

let x be set ; :: thesis: ( x in rng f implies x is Function )
assume x in rng f ; :: thesis: x is Function
then ex y being set st
( y in dom f & x = f . y ) by FUNCT_1:def 3;
hence x is Function ; :: thesis: verum

end;

then for x being set holds
( x in rng f iff ( x in rng f & x is Function ) ) ;
hence SubFuncs (rng f) = rng f by FUNCT_6:def 1; :: thesis: verum