let X be set ; :: thesis: ( ( for x being set st x in X holds
x is Function ) implies SubFuncs X = X )
assume for x being set st x in X holds
x is Function ; :: thesis: SubFuncs X = X
then for x being set holds
( x in X iff ( x in X & x is Function ) ) ;
hence SubFuncs X = X by Def1; :: thesis: verum