A2: Im f is_integrable_on M by A1, Def4;
then A3: -infty < Integral M,(Im f) by MESFUNC6:90;
A4: Re f is_integrable_on M by A1, Def4;
then A5: Integral M,(Re f) < +infty by MESFUNC6:90;
A6: Integral M,(Im f) < +infty by A2, MESFUNC6:90;
-infty < Integral M,(Re f) by A4, MESFUNC6:90;
then reconsider R = Integral M,(Re f), I = Integral M,(Im f) as Real by A5, A3, A6, XXREAL_0:14;
take IT = R + (I * <i> ); :: thesis: ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & IT = R + (I * <i> ) )
thus ex R, I being Real st
( R = Integral M,(Re f) & I = Integral M,(Im f) & IT = R + (I * <i> ) ) ; :: thesis: verum