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