let f be Element of HFuncs X; :: thesis: f is homogeneous
f in HFuncs X ;
then ex g being Element of PFuncs ((X *),X) st
( f = g & g is homogeneous ) ;
hence f is homogeneous ; :: thesis: verum