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

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