let A be 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
integral f,A = integral g
let f be PartFunc of REAL ,COMPLEX ; :: thesis: for g being Function of A,COMPLEX st f | A = g holds
integral f,A = integral g
let g be Function of A,COMPLEX ; :: thesis: ( f | A = g implies integral f,A = integral g )
assume A1: f | A = g ; :: thesis: integral f,A = integral g
A2: A = dom g by FUNCT_2:def 1
.= (dom f) /\ A by A1, RELAT_1:90 ;
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 ;
dom g = A by FUNCT_2:def 1;
then reconsider g0 = g as PartFunc of REAL ,COMPLEX by RELSET_1:13;
X1: Re g = Re g0
.= F by A1, Lm6 ;
A = (dom (Im f)) /\ A by A2, 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 ;
Im g = Im g0
.= G by A1, Lm6 ;
hence integral f,A = integral g by X1; :: thesis: verum