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:26;
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 non empty closed_interval Subset of REAL by A1, MEASURE5:14;
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 7
.= ((dom u01) /\ Z1) /\ ((dom v01) /\ Z1) by A2, FDIFF_1:def 7
.= (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 7
.= ((dom u02) /\ Z2) /\ ((dom v02) /\ Z2) by A1, FDIFF_1:def 7
.= (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:61
.= ((dom u01) /\ (dom v01)) /\ (Z1 /\ AB) by A6, XBOOLE_1:16
.= ((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:61
.= ((dom u01) /\ (dom v01)) /\ (Z2 /\ AB) by A7, XBOOLE_1:16
.= ((dom u01) /\ (dom v01)) /\ AB by A1, XBOOLE_1:1, XBOOLE_1:28 ;
for x0 being object 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 object ; :: 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:61;
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 7;
reconsider x0 = x0 as Real by A11;
A14: (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = ((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) . x0 by A10, FUNCT_1:47
.= ((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 7 ;
x0 in (dom ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2)))) /\ AB by A8, A9, A10, RELAT_1:61;
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 7;
(((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0 = ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) . x0 by A8, A9, A10, FUNCT_1:47
.= ((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 7 ;
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 7;
hence (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0 by A2, A13, A14, FDIFF_1:def 7; :: thesis: verum

end;

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

end;

A18: 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 ;
A19: ((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 A20: dom ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) = ((dom v01) /\ Z1) /\ ((dom u01) /\ (dom (y `| Z1))) by A2, FDIFF_1:def 7
.= ((dom v01) /\ Z1) /\ ((dom u01) /\ Z1) by A2, FDIFF_1:def 7
.= (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 A21: dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) = ((dom v02) /\ Z2) /\ ((dom u02) /\ (dom (y `| Z2))) by A1, FDIFF_1:def 7
.= ((dom v02) /\ Z2) /\ ((dom u02) /\ Z2) by A1, FDIFF_1:def 7
.= (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 ;
A22: dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) = (dom ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1)))) /\ AB by RELAT_1:61
.= ((dom v01) /\ (dom u01)) /\ (Z1 /\ AB) by A20, XBOOLE_1:16
.= ((dom v01) /\ (dom u01)) /\ AB by A1, XBOOLE_1:28 ;
A23: dom (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) = (dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2)))) /\ AB by RELAT_1:61
.= ((dom v01) /\ (dom u01)) /\ (Z2 /\ AB) by A21, XBOOLE_1:16
.= ((dom v01) /\ (dom u01)) /\ AB by A1, XBOOLE_1:1, XBOOLE_1:28 ;
for x0 being object 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 object ; :: 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 A24: 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 A24, RELAT_1:61;
then A25: 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 A26: ( x0 in dom (v01 (#) (x `| Z1)) & x0 in dom (u01 (#) (y `| Z1)) ) by XBOOLE_0:def 4;
then A27: ( 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 7;
reconsider x0 = x0 as Real by A27;
(((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) . x0 by A24, FUNCT_1:47
.= ((v01 (#) (x `| Z1)) . x0) + ((u01 (#) (y `| Z1)) . x0) by A25, VALUED_1:def 1
.= ((v01 . x0) * ((x `| Z1) . x0)) + ((u01 (#) (y `| Z1)) . x0) by A26, VALUED_1:def 4
.= ((v01 . x0) * ((x `| Z1) . x0)) + ((u01 . x0) * ((y `| Z1) . x0)) by A26, VALUED_1:def 4
.= ((v01 . x0) * (diff (x,x0))) + ((u01 . x0) * ((y `| Z1) . x0)) by A2, A28, FDIFF_1:def 7 ;
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 7;
x0 in (dom ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2)))) /\ AB by A22, A23, A24, RELAT_1:61;
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 7;
(((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0 = ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) . x0 by A22, A23, A24, FUNCT_1:47
.= ((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 7 ;
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 7; :: thesis: verum

end;

hence ((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB = ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB by A22, A23, FUNCT_1:def 11; :: 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 A19
.= 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, A18; :: thesis: verum