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 )

proof

assume A2: f is_integrable_on A ; :: thesis: g is integrable
( Re g is integrable & Im g is integrable )

proof

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, Def9;
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, INTEGRA5:def 1; :: 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, Def9;
Im g = Im g0
.= G by A1, Lm4 ;
hence Im g is integrable by A5, INTEGRA5:def 1; :: thesis: verum

end;

hence g is integrable by Def7; :: thesis: verum

end;

assume A6: g is integrable ; :: thesis: f is_integrable_on A
( Re f is_integrable_on A & Im f is_integrable_on A )

proof

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
.= (Re f) || A by A1, Lm4 ;
then (Re f) || A is integrable by A6, Def7;
hence Re f is_integrable_on A by INTEGRA5:def 1; :: thesis: Im f is_integrable_on A
Im g = Im g0
.= (Im f) || A by A1, Lm4 ;
then (Im f) || A is integrable by A6, Def7;
hence Im f is_integrable_on A by INTEGRA5:def 1; :: thesis: verum

end;

hence f is_integrable_on A by Def9; :: thesis: verum