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