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>)
; 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>) )
; verum