A2: Im f is_integrable_on M by A1;
then A3: -infty < Integral (M,(Im f)) by MESFUNC6:90;
A4: Re f is_integrable_on M by A1;
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 Element of REAL by A5, A3, A6, XXREAL_0:14;
take R + (I * <i>) ; :: thesis: ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & R + (I * <i>) = R + (I * <i>) )
thus ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & R + (I * <i>) = R + (I * <i>) ) ; :: thesis: verum