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