Up (p,T,1) = HM (p,T) by Th36;
hence ( Up (p,T,1) is non-zero & Up (p,T,1) is monomial-like ) ; :: thesis: verum