let a, b be Real; :: thesis: for x, y being PartFunc of REAL ,REAL
for Z1, Z2 being Subset of REAL
for f being PartFunc of COMPLEX ,COMPLEX st a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y & Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 & x is_differentiable_on Z2 & y is_differentiable_on Z2 & rng ((x + (<i> (#) y)) | [.a,b.]) c= dom f holds
integral f,x,y,a,b,Z1 = integral f,x,y,a,b,Z2
let x, y be PartFunc of REAL ,REAL ; :: thesis: for Z1, Z2 being Subset of REAL
for f being PartFunc of COMPLEX ,COMPLEX st a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y & Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 & x is_differentiable_on Z2 & y is_differentiable_on Z2 & rng ((x + (<i> (#) y)) | [.a,b.]) c= dom f holds
integral f,x,y,a,b,Z1 = integral f,x,y,a,b,Z2
let Z1, Z2 be Subset of REAL ; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX st a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y & Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 & x is_differentiable_on Z2 & y is_differentiable_on Z2 & rng ((x + (<i> (#) y)) | [.a,b.]) c= dom f holds
integral f,x,y,a,b,Z1 = integral f,x,y,a,b,Z2
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y & Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 & x is_differentiable_on Z2 & y is_differentiable_on Z2 & rng ((x + (<i> (#) y)) | [.a,b.]) c= dom f implies integral f,x,y,a,b,Z1 = integral f,x,y,a,b,Z2 )
assume A1: ( a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y & Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 & x is_differentiable_on Z2 & y is_differentiable_on Z2 & rng ((x + (<i> (#) y)) | [.a,b.]) c= dom f ) ; :: thesis: integral f,x,y,a,b,Z1 = integral f,x,y,a,b,Z2
then A2: ( x is_differentiable_on Z1 & y is_differentiable_on Z1 ) by FDIFF_1:34;
consider u01, v01 being PartFunc of REAL ,REAL such that
A3: ( u01 = ((Re f) * R2-to-C ) * <:x,y:> & v01 = ((Im f) * R2-to-C ) * <:x,y:> & integral f,x,y,a,b,Z1 = (integral ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))),a,b) + ((integral ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))),a,b) * <i> ) ) by Def2;
consider u02, v02 being PartFunc of REAL ,REAL such that
A4: ( u02 = ((Re f) * R2-to-C ) * <:x,y:> & v02 = ((Im f) * R2-to-C ) * <:x,y:> & integral f,x,y,a,b,Z2 = (integral ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))),a,b) + ((integral ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))),a,b) * <i> ) ) by Def2;
reconsider AB = [.a,b.] as closed-interval Subset of REAL by A1, INTEGRA1:def 1;
A5: ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB = ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB

proof

dom ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) = (dom (u01 (#) (x `| Z1))) /\ (dom (v01 (#) (y `| Z1))) by VALUED_1:12
.= ((dom u01) /\ (dom (x `| Z1))) /\ (dom (v01 (#) (y `| Z1))) by VALUED_1:def 4
.= ((dom u01) /\ (dom (x `| Z1))) /\ ((dom v01) /\ (dom (y `| Z1))) by VALUED_1:def 4 ;
then A6: dom ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) = ((dom u01) /\ Z1) /\ ((dom v01) /\ (dom (y `| Z1))) by A2, FDIFF_1:def 8
.= ((dom u01) /\ Z1) /\ ((dom v01) /\ Z1) by A2, FDIFF_1:def 8
.= (dom u01) /\ (Z1 /\ ((dom v01) /\ Z1)) by XBOOLE_1:16
.= (dom u01) /\ ((Z1 /\ Z1) /\ (dom v01)) by XBOOLE_1:16
.= ((dom u01) /\ (dom v01)) /\ Z1 by XBOOLE_1:16 ;
dom ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) = (dom (u02 (#) (x `| Z2))) /\ (dom (v02 (#) (y `| Z2))) by VALUED_1:12
.= ((dom u02) /\ (dom (x `| Z2))) /\ (dom (v02 (#) (y `| Z2))) by VALUED_1:def 4
.= ((dom u02) /\ (dom (x `| Z2))) /\ ((dom v02) /\ (dom (y `| Z2))) by VALUED_1:def 4 ;
then A7: dom ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) = ((dom u02) /\ Z2) /\ ((dom v02) /\ (dom (y `| Z2))) by A1, FDIFF_1:def 8
.= ((dom u02) /\ Z2) /\ ((dom v02) /\ Z2) by A1, FDIFF_1:def 8
.= (dom u02) /\ (Z2 /\ ((dom v02) /\ Z2)) by XBOOLE_1:16
.= (dom u02) /\ ((Z2 /\ Z2) /\ (dom v02)) by XBOOLE_1:16
.= ((dom u01) /\ (dom v01)) /\ Z2 by A3, A4, XBOOLE_1:16 ;
A8: dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) = (dom ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1)))) /\ AB by RELAT_1:90
.= ((dom u01) /\ (dom v01)) /\ (Z1 /\ AB) by XBOOLE_1:16, A6
.= ((dom u01) /\ (dom v01)) /\ AB by A1, XBOOLE_1:28 ;
A9: dom (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) = (dom ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2)))) /\ AB by RELAT_1:90
.= ((dom u01) /\ (dom v01)) /\ (Z2 /\ AB) by XBOOLE_1:16, A7
.= ((dom u01) /\ (dom v01)) /\ AB by A1, XBOOLE_1:28, XBOOLE_1:1 ;
for x0 being set st x0 in dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) holds
(((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) implies (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0 )
assume A10: x0 in dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) ; :: thesis: (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0
x0 in (dom ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1)))) /\ AB by A10, RELAT_1:90;
then A11: x0 in dom ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) by XBOOLE_0:def 4;
then x0 in (dom (u01 (#) (x `| Z1))) /\ (dom (v01 (#) (y `| Z1))) by VALUED_1:12;
then A12: ( x0 in dom (u01 (#) (x `| Z1)) & x0 in dom (v01 (#) (y `| Z1)) ) by XBOOLE_0:def 4;
then ( x0 in (dom u01) /\ (dom (x `| Z1)) & x0 in (dom v01) /\ (dom (y `| Z1)) ) by VALUED_1:def 4;
then ( x0 in dom u01 & x0 in dom (x `| Z1) & x0 in dom v01 & x0 in dom (y `| Z1) ) by XBOOLE_0:def 4;
then A13: x0 in Z1 by A2, FDIFF_1:def 8;
reconsider x0 = x0 as Real by A10;
A14: (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) . x0 by A10, FUNCT_1:70
.= ((u01 (#) (x `| Z1)) . x0) - ((v01 (#) (y `| Z1)) . x0) by A11, VALUED_1:13
.= ((u01 . x0) * ((x `| Z1) . x0)) - ((v01 (#) (y `| Z1)) . x0) by A12, VALUED_1:def 4
.= ((u01 . x0) * ((x `| Z1) . x0)) - ((v01 . x0) * ((y `| Z1) . x0)) by A12, VALUED_1:def 4
.= ((u01 . x0) * (diff x,x0)) - ((v01 . x0) * ((y `| Z1) . x0)) by A2, A13, FDIFF_1:def 8 ;
x0 in (dom ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2)))) /\ AB by A8, A9, A10, RELAT_1:90;
then A15: x0 in dom ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) by XBOOLE_0:def 4;
then x0 in (dom (u02 (#) (x `| Z2))) /\ (dom (v02 (#) (y `| Z2))) by VALUED_1:12;
then A16: ( x0 in dom (u02 (#) (x `| Z2)) & x0 in dom (v02 (#) (y `| Z2)) ) by XBOOLE_0:def 4;
then ( x0 in (dom u02) /\ (dom (x `| Z2)) & x0 in (dom v02) /\ (dom (y `| Z2)) ) by VALUED_1:def 4;
then ( x0 in dom u02 & x0 in dom (x `| Z2) & x0 in dom v02 & x0 in dom (y `| Z2) ) by XBOOLE_0:def 4;
then A17: x0 in Z2 by A1, FDIFF_1:def 8;
(((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0 = ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) . x0 by A8, A9, A10, FUNCT_1:70
.= ((u02 (#) (x `| Z2)) . x0) - ((v02 (#) (y `| Z2)) . x0) by A15, VALUED_1:13
.= ((u02 . x0) * ((x `| Z2) . x0)) - ((v02 (#) (y `| Z2)) . x0) by A16, VALUED_1:def 4
.= ((u02 . x0) * ((x `| Z2) . x0)) - ((v02 . x0) * ((y `| Z2) . x0)) by A16, VALUED_1:def 4
.= ((u02 . x0) * (diff x,x0)) - ((v02 . x0) * ((y `| Z2) . x0)) by A1, A17, FDIFF_1:def 8 ;
then (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0 = ((u01 . x0) * (diff x,x0)) - ((v01 . x0) * (diff y,x0)) by A1, A3, A4, A17, FDIFF_1:def 8;
hence (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0 by A2, A13, A14, FDIFF_1:def 8; :: thesis: verum

end;

hence ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB = ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB by A8, A9, FUNCT_1:def 17; :: thesis: verum

end;

A19: integral ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))),a,b = integral ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))),AB by INTEGRA5:19
.= integral ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))),AB by A5
.= integral ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))),a,b by INTEGRA5:19 ;
A20: ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB = ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB

proof

dom ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) = (dom (v01 (#) (x `| Z1))) /\ (dom (u01 (#) (y `| Z1))) by VALUED_1:def 1
.= ((dom v01) /\ (dom (x `| Z1))) /\ (dom (u01 (#) (y `| Z1))) by VALUED_1:def 4
.= ((dom v01) /\ (dom (x `| Z1))) /\ ((dom u01) /\ (dom (y `| Z1))) by VALUED_1:def 4 ;
then A21: dom ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) = ((dom v01) /\ Z1) /\ ((dom u01) /\ (dom (y `| Z1))) by A2, FDIFF_1:def 8
.= ((dom v01) /\ Z1) /\ ((dom u01) /\ Z1) by A2, FDIFF_1:def 8
.= (dom v01) /\ (Z1 /\ ((dom u01) /\ Z1)) by XBOOLE_1:16
.= (dom v01) /\ ((Z1 /\ Z1) /\ (dom u01)) by XBOOLE_1:16
.= ((dom v01) /\ (dom u01)) /\ Z1 by XBOOLE_1:16 ;
dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) = (dom (v02 (#) (x `| Z2))) /\ (dom (u02 (#) (y `| Z2))) by VALUED_1:def 1
.= ((dom v02) /\ (dom (x `| Z2))) /\ (dom (u02 (#) (y `| Z2))) by VALUED_1:def 4
.= ((dom v02) /\ (dom (x `| Z2))) /\ ((dom u02) /\ (dom (y `| Z2))) by VALUED_1:def 4 ;
then A22: dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) = ((dom v02) /\ Z2) /\ ((dom u02) /\ (dom (y `| Z2))) by A1, FDIFF_1:def 8
.= ((dom v02) /\ Z2) /\ ((dom u02) /\ Z2) by A1, FDIFF_1:def 8
.= (dom v02) /\ (Z2 /\ ((dom u02) /\ Z2)) by XBOOLE_1:16
.= (dom v02) /\ ((Z2 /\ Z2) /\ (dom u02)) by XBOOLE_1:16
.= ((dom v01) /\ (dom u01)) /\ Z2 by A3, A4, XBOOLE_1:16 ;
A23: dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) = (dom ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1)))) /\ AB by RELAT_1:90
.= ((dom v01) /\ (dom u01)) /\ (Z1 /\ AB) by XBOOLE_1:16, A21
.= ((dom v01) /\ (dom u01)) /\ AB by A1, XBOOLE_1:28 ;
A24: dom (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) = (dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2)))) /\ AB by RELAT_1:90
.= ((dom v01) /\ (dom u01)) /\ (Z2 /\ AB) by XBOOLE_1:16, A22
.= ((dom v01) /\ (dom u01)) /\ AB by A1, XBOOLE_1:1, XBOOLE_1:28 ;
for x0 being set st x0 in dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) holds
(((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) implies (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0 )
assume A25: x0 in dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) ; :: thesis: (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0
x0 in (dom ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1)))) /\ AB by A25, RELAT_1:90;
then A26: x0 in dom ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) by XBOOLE_0:def 4;
then x0 in (dom (v01 (#) (x `| Z1))) /\ (dom (u01 (#) (y `| Z1))) by VALUED_1:def 1;
then A27: ( x0 in dom (v01 (#) (x `| Z1)) & x0 in dom (u01 (#) (y `| Z1)) ) by XBOOLE_0:def 4;
then ( x0 in (dom v01) /\ (dom (x `| Z1)) & x0 in (dom u01) /\ (dom (y `| Z1)) ) by VALUED_1:def 4;
then ( x0 in dom v01 & x0 in dom (x `| Z1) & x0 in dom u01 & x0 in dom (y `| Z1) ) by XBOOLE_0:def 4;
then A28: x0 in Z1 by A2, FDIFF_1:def 8;
reconsider x0 = x0 as Real by A25;
(((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) . x0 by A25, FUNCT_1:70
.= ((v01 (#) (x `| Z1)) . x0) + ((u01 (#) (y `| Z1)) . x0) by A26, VALUED_1:def 1
.= ((v01 . x0) * ((x `| Z1) . x0)) + ((u01 (#) (y `| Z1)) . x0) by A27, VALUED_1:def 4
.= ((v01 . x0) * ((x `| Z1) . x0)) + ((u01 . x0) * ((y `| Z1) . x0)) by A27, VALUED_1:def 4
.= ((v01 . x0) * (diff x,x0)) + ((u01 . x0) * ((y `| Z1) . x0)) by A2, A28, FDIFF_1:def 8 ;
then A29: (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = ((v01 . x0) * (diff x,x0)) + ((u01 . x0) * (diff y,x0)) by A2, A28, FDIFF_1:def 8;
x0 in (dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2)))) /\ AB by A23, A24, A25, RELAT_1:90;
then A30: x0 in dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) by XBOOLE_0:def 4;
then x0 in (dom (v02 (#) (x `| Z2))) /\ (dom (u02 (#) (y `| Z2))) by VALUED_1:def 1;
then A31: ( x0 in dom (v02 (#) (x `| Z2)) & x0 in dom (u02 (#) (y `| Z2)) ) by XBOOLE_0:def 4;
then ( x0 in (dom v02) /\ (dom (x `| Z2)) & x0 in (dom u02) /\ (dom (y `| Z2)) ) by VALUED_1:def 4;
then ( x0 in dom v02 & x0 in dom (x `| Z2) & x0 in dom u02 & x0 in dom (y `| Z2) ) by XBOOLE_0:def 4;
then A32: x0 in Z2 by A1, FDIFF_1:def 8;
(((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0 = ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) . x0 by A23, A24, A25, FUNCT_1:70
.= ((v02 (#) (x `| Z2)) . x0) + ((u02 (#) (y `| Z2)) . x0) by A30, VALUED_1:def 1
.= ((v02 . x0) * ((x `| Z2) . x0)) + ((u02 (#) (y `| Z2)) . x0) by A31, VALUED_1:def 4
.= ((v02 . x0) * ((x `| Z2) . x0)) + ((u02 . x0) * ((y `| Z2) . x0)) by A31, VALUED_1:def 4
.= ((v02 . x0) * (diff x,x0)) + ((u02 . x0) * ((y `| Z2) . x0)) by A1, A32, FDIFF_1:def 8 ;
hence (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0 by A1, A3, A4, A29, A32, FDIFF_1:def 8; :: thesis: verum

end;

hence ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB = ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB by A23, A24, FUNCT_1:def 17; :: thesis: verum

end;

integral ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))),a,b = integral ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))),AB by INTEGRA5:19
.= integral ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))),AB by A20
.= integral ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))),a,b by INTEGRA5:19 ;
hence integral f,x,y,a,b,Z1 = integral f,x,y,a,b,Z2 by A3, A4, A19; :: thesis: verum