let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,COMPLEX

for g being Function of A,COMPLEX st f | A = g holds

( f is_integrable_on A iff g is integrable )

let f be PartFunc of REAL,COMPLEX; :: thesis: for g being Function of A,COMPLEX st f | A = g holds

( f is_integrable_on A iff g is integrable )

let g be Function of A,COMPLEX; :: thesis: ( f | A = g implies ( f is_integrable_on A iff g is integrable ) )

assume A1: f | A = g ; :: thesis: ( f is_integrable_on A iff g is integrable )

thus ( f is_integrable_on A implies g is integrable ) :: thesis: ( g is integrable implies f is_integrable_on A )

( Re f is_integrable_on A & Im f is_integrable_on A ) by A1, Lm4, A6;

hence f is_integrable_on A ; :: thesis: verum

for g being Function of A,COMPLEX st f | A = g holds

( f is_integrable_on A iff g is integrable )

let f be PartFunc of REAL,COMPLEX; :: thesis: for g being Function of A,COMPLEX st f | A = g holds

( f is_integrable_on A iff g is integrable )

let g be Function of A,COMPLEX; :: thesis: ( f | A = g implies ( f is_integrable_on A iff g is integrable ) )

assume A1: f | A = g ; :: thesis: ( f is_integrable_on A iff g is integrable )

thus ( f is_integrable_on A implies g is integrable ) :: thesis: ( g is integrable implies f is_integrable_on A )

proof

assume A6:
g is integrable
; :: thesis: f is_integrable_on A
assume A2:
f is_integrable_on A
; :: thesis: g is integrable

( Re g is integrable & Im g is integrable )

end;( Re g is integrable & Im g is integrable )

proof

hence
g is integrable
; :: thesis: verum
A3: A =
dom g
by FUNCT_2:def 1

.= (dom f) /\ A by A1, RELAT_1:61 ;

then A = (dom (Re f)) /\ A by COMSEQ_3:def 3;

then (Re f) || A is total by INTEGRA5:6, XBOOLE_1:17;

then reconsider F = (Re f) | A as Function of A,REAL ;

A4: Re f is_integrable_on A by A2;

dom g = A by FUNCT_2:def 1;

then reconsider g0 = g as PartFunc of REAL,COMPLEX by RELSET_1:5;

Re g = Re g0

.= F by A1, Lm4 ;

hence Re g is integrable by A4; :: thesis: Im g is integrable

A = (dom (Im f)) /\ A by A3, COMSEQ_3:def 4;

then (Im f) || A is total by INTEGRA5:6, XBOOLE_1:17;

then reconsider G = (Im f) | A as Function of A,REAL ;

A5: Im f is_integrable_on A by A2;

Im g = Im g0

.= G by A1, Lm4 ;

hence Im g is integrable by A5; :: thesis: verum

end;.= (dom f) /\ A by A1, RELAT_1:61 ;

then A = (dom (Re f)) /\ A by COMSEQ_3:def 3;

then (Re f) || A is total by INTEGRA5:6, XBOOLE_1:17;

then reconsider F = (Re f) | A as Function of A,REAL ;

A4: Re f is_integrable_on A by A2;

dom g = A by FUNCT_2:def 1;

then reconsider g0 = g as PartFunc of REAL,COMPLEX by RELSET_1:5;

Re g = Re g0

.= F by A1, Lm4 ;

hence Re g is integrable by A4; :: thesis: Im g is integrable

A = (dom (Im f)) /\ A by A3, COMSEQ_3:def 4;

then (Im f) || A is total by INTEGRA5:6, XBOOLE_1:17;

then reconsider G = (Im f) | A as Function of A,REAL ;

A5: Im f is_integrable_on A by A2;

Im g = Im g0

.= G by A1, Lm4 ;

hence Im g is integrable by A5; :: thesis: verum

( Re f is_integrable_on A & Im f is_integrable_on A ) by A1, Lm4, A6;

hence f is_integrable_on A ; :: thesis: verum