let f, g, h be Function; :: thesis: ( SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
thus SubFuncs {} = {} by Th27, XBOOLE_1:3; :: thesis: ( SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
for x being set st x in {f} holds
x is Function ;
hence SubFuncs {f} = {f} by Lm1; :: thesis: ( SubFuncs {f,g} = {f,g} & SubFuncs {f,g,h} = {f,g,h} )
for x being set st x in {f,g} holds
x is Function ;
hence SubFuncs {f,g} = {f,g} by Lm1; :: thesis: SubFuncs {f,g,h} = {f,g,h}
for x being set st x in {f,g,h} holds
x is Function by ENUMSET1:def 1;
hence SubFuncs {f,g,h} = {f,g,h} by Lm1; :: thesis: verum