( Re f is_integrable_on M & Im f is_integrable_on M ) by AS, Def4;
then ( -infty < Integral M,(Re f) & Integral M,(Re f) < +infty & -infty < Integral M,(Im f) & Integral M,(Im f) < +infty ) by MESFUNC6:90;
then reconsider R = Integral M,(Re f), I = Integral M,(Im f) as Real by 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