f is_integrable_on P2M P by A1, Def3;
then ( -infty < Integral ((P2M P),f) & Integral ((P2M P),f) < +infty ) by MESFUNC6:90;
hence Integral ((P2M P),f) is Element of REAL by XXREAL_0:48; :: thesis: verum