let f be Element of HFuncs X; :: thesis: f is homogeneous
( HFuncs X = { g where g is Element of PFuncs (X * ),X : g 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