let f be PartFunc of COMPLEX,COMPLEX; :: thesis:
let C, C1, C2 be C1-curve; :: thesis:
let a, b, d be Real; :: thesis:
assume A1: ( rng C c= dom f & f is_integrable_on C & f is_bounded_on C & a <= b & dom C = [.a,b.] & d in [.a,b.] & dom C1 = [.a,d.] & dom C2 = [.d,b.] & ( for t being Real st t in dom C1 holds
C . t = C1 . t ) & ( for t being Real st t in dom C2 holds
C . t = C2 . t ) ) ; :: thesis:
A2: ( a <= d & d <= b ) by A1, XXREAL_1:1;
consider a0, b0 being Real, x, y being PartFunc of REAL,REAL, Z being Subset of REAL such that
A3: ( a0 <= b0 & [.a0,b0.] = dom C & [.a0,b0.] c= dom x & [.a0,b0.] c= dom y & Z is open & [.a0,b0.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + ( (#) y)) | [.a0,b0.] ) by Def3;
A4: ( a0 = a & b0 = b )

proof

thus a0 = inf [.a0,b0.] by A3, XXREAL_2:25
.= a by A1, A3, XXREAL_2:25 ; :: thesis:
thus b0 = sup [.a0,b0.] by A3, XXREAL_2:29
.= b by A1, A3, XXREAL_2:29 ; :: thesis:

end;

consider u0, v0 being PartFunc of REAL,REAL such that
A5: ( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & integral (f,x,y,a,b,Z) = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * ) ) by Def2;
consider a1, b1 being Real, x1, y1 being PartFunc of REAL,REAL, Z1 being Subset of REAL such that
A6: ( a1 <= b1 & [.a1,b1.] = dom C1 & [.a1,b1.] c= dom x1 & [.a1,b1.] c= dom y1 & Z1 is open & [.a1,b1.] c= Z1 & x1 is_differentiable_on Z1 & y1 is_differentiable_on Z1 & x1 `| Z1 is continuous & y1 `| Z1 is continuous & C1 = (x1 + ( (#) y1)) | [.a1,b1.] ) by Def3;
A7: ( a1 = a & b1 = d )

proof

thus a1 = inf [.a1,b1.] by A6, XXREAL_2:25
.= a by A2, A1, A6, XXREAL_2:25 ; :: thesis:
thus b1 = sup [.a1,b1.] by A6, XXREAL_2:29
.= d by A2, A1, A6, XXREAL_2:29 ; :: thesis:

end;

A8: rng C1 c= dom f

proof

A9: [.a,d.] c= [.a,b.] by A2, XXREAL_1:34;
for y0 being object st y0 in rng C1 holds
y0 in rng C

proof

let y0 be object ; :: thesis:
assume A10: y0 in rng C1 ; :: thesis:
consider x0 being object such that
A11: ( x0 in dom C1 & y0 = C1 . x0 ) by A10, FUNCT_1:def 3;
C1 . x0 = C . x0 by A1, A11;
hence y0 in rng C by A1, A9, A11, FUNCT_1:3; :: thesis:

end;

then rng C1 c= rng C ;
hence rng C1 c= dom f by A1; :: thesis:

end;

consider a2, b2 being Real, x2, y2 being PartFunc of REAL,REAL, Z2 being Subset of REAL such that
A12: ( a2 <= b2 & [.a2,b2.] = dom C2 & [.a2,b2.] c= dom x2 & [.a2,b2.] c= dom y2 & Z2 is open & [.a2,b2.] c= Z2 & x2 is_differentiable_on Z2 & y2 is_differentiable_on Z2 & x2 `| Z2 is continuous & y2 `| Z2 is continuous & C2 = (x2 + ( (#) y2)) | [.a2,b2.] ) by Def3;
A13: ( a2 = d & b2 = b )

proof

thus a2 = inf [.a2,b2.] by A12, XXREAL_2:25
.= d by A2, A1, A12, XXREAL_2:25 ; :: thesis:
thus b2 = sup [.a2,b2.] by A12, XXREAL_2:29
.= b by A2, A1, A12, XXREAL_2:29 ; :: thesis:

end;

rng C2 c= dom f

proof

A14: [.d,b.] c= [.a,b.] by A2, XXREAL_1:34;
for y0 being object st y0 in rng C2 holds
y0 in rng C

proof

let y0 be object ; :: thesis:
assume A15: y0 in rng C2 ; :: thesis:
consider x0 being object such that
A16: ( x0 in dom C2 & y0 = C2 . x0 ) by A15, FUNCT_1:def 3;
C2 . x0 = C . x0 by A1, A16;
hence y0 in rng C by A1, A14, A16, FUNCT_1:3; :: thesis:

end;

then rng C2 c= rng C ;
hence rng C2 c= dom f by A1; :: thesis:

end;

then A17: integral (f,C2) = integral (f,x2,y2,d,b,Z2) by A12, A13, Def4;
A18: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A19: ['a,b'] c= dom u0

proof

for x0 being object st x0 in [.a,b.] holds
x0 in dom u0

proof

let x0 be object ; :: thesis:
assume A20: x0 in [.a,b.] ; :: thesis:
A21: C . x0 in rng C by A3, A4, A20, FUNCT_1:3;
A22: ( x0 in dom x & x0 in dom y ) by A3, A4, A20;
A23: x0 in (dom x) /\ (dom y) by A3, A4, A20, XBOOLE_0:def 4;
then A24: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:> . x0;
reconsider xx0 = x . x0, yx0 = y . x0 as Element of REAL by XREAL_0:def 1;
<:x,y:> . x0 = [xx0,yx0] by A23, FUNCT_3:48;
then <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def 2;
then A25: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def 1;
x0 in dom ( (#) y) by A22, VALUED_1:def 5;
then x0 in (dom x) /\ (dom ( (#) y)) by A3, A4, A20, XBOOLE_0:def 4;
then A26: x0 in dom (x + ( (#) y)) by VALUED_1:def 1;
A27: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A28: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + ( (#) y)) . x0 by A20, A3, A4, FUNCT_1:49
.= (x . x0) + (( (#) y) . x0) by A26, VALUED_1:def 1
.= (x . x0) + ( * (y . x0)) by VALUED_1:6
.= R2-to-C . [xx0,yx0] by A27, A28, Def1
.= R2-to-C . (<:x,y:> . x0) by A23, FUNCT_3:48 ;
then R2-to-C . (<:x,y:> . x0) in dom f by A1, A21;
then R2-to-C . (<:x,y:> . x0) in dom (Re f) by COMSEQ_3:def 3;
then <:x,y:> . x0 in dom ((Re f) * R2-to-C) by A25, FUNCT_1:11;
hence x0 in dom u0 by A5, A24, FUNCT_1:11; :: thesis:

end;

hence ['a,b'] c= dom u0 by A18; :: thesis:

end;

A29: ['a,b'] c= dom v0

proof

for x0 being object st x0 in [.a,b.] holds
x0 in dom v0

proof

let x0 be object ; :: thesis:
assume A30: x0 in [.a,b.] ; :: thesis:
A31: C . x0 in rng C by A3, A4, A30, FUNCT_1:3;
A32: ( x0 in dom x & x0 in dom y ) by A3, A4, A30;
A33: x0 in (dom x) /\ (dom y) by A3, A4, A30, XBOOLE_0:def 4;
then A34: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:> . x0;
reconsider xx0 = x . x0, yx0 = y . x0 as Element of REAL by XREAL_0:def 1;
<:x,y:> . x0 = [xx0,yx0] by A33, FUNCT_3:48;
then <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def 2;
then A35: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def 1;
x0 in dom ( (#) y) by A32, VALUED_1:def 5;
then x0 in (dom x) /\ (dom ( (#) y)) by A3, A4, A30, XBOOLE_0:def 4;
then A36: x0 in dom (x + ( (#) y)) by VALUED_1:def 1;
A37: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A38: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + ( (#) y)) . x0 by A30, A3, A4, FUNCT_1:49
.= (x . x0) + (( (#) y) . x0) by A36, VALUED_1:def 1
.= (x . x0) + ( * (y . x0)) by VALUED_1:6
.= R2-to-C . [xx0,yx0] by A37, A38, Def1
.= R2-to-C . (<:x,y:> . x0) by A33, FUNCT_3:48 ;
then R2-to-C . (<:x,y:> . x0) in dom f by A1, A31;
then R2-to-C . (<:x,y:> . x0) in dom (Im f) by COMSEQ_3:def 4;
then <:x,y:> . x0 in dom ((Im f) * R2-to-C) by A35, FUNCT_1:11;
hence x0 in dom v0 by A5, A34, FUNCT_1:11; :: thesis:

end;

hence ['a,b'] c= dom v0 by A18; :: thesis:

end;

A39: ( (u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is_integrable_on ['a,b'] & (v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is_integrable_on ['a,b'] ) by A1, A3;
A40: ( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded & ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded ) by A1, A3;
A41: ['a,b'] c= dom ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z)))

proof

A42: dom ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) = (dom (u0 (#) (x `| Z))) /\ (dom (v0 (#) (y `| Z))) by VALUED_1:12
.= ((dom u0) /\ (dom (x `| Z))) /\ (dom (v0 (#) (y `| Z))) by VALUED_1:def 4
.= ((dom u0) /\ (dom (x `| Z))) /\ ((dom v0) /\ (dom (y `| Z))) by VALUED_1:def 4
.= ((dom u0) /\ Z) /\ ((dom v0) /\ (dom (y `| Z))) by A3, FDIFF_1:def 7
.= ((dom u0) /\ Z) /\ ((dom v0) /\ Z) by A3, FDIFF_1:def 7
.= (dom u0) /\ (Z /\ ((dom v0) /\ Z)) by XBOOLE_1:16
.= (dom u0) /\ ((Z /\ Z) /\ (dom v0)) by XBOOLE_1:16
.= ((dom u0) /\ (dom v0)) /\ Z by XBOOLE_1:16 ;
A43: ['a,b'] c= (dom u0) /\ (dom v0) by A19, A29, XBOOLE_1:19;
['a,b'] c= Z by A1, A3, INTEGRA5:def 3;
hence ['a,b'] c= dom ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) by A42, A43, XBOOLE_1:19; :: thesis:

end;

A44: ['a,b'] c= dom ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z)))

proof

A45: dom ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) = (dom (v0 (#) (x `| Z))) /\ (dom (u0 (#) (y `| Z))) by VALUED_1:def 1
.= ((dom v0) /\ (dom (x `| Z))) /\ (dom (u0 (#) (y `| Z))) by VALUED_1:def 4
.= ((dom v0) /\ (dom (x `| Z))) /\ ((dom u0) /\ (dom (y `| Z))) by VALUED_1:def 4
.= ((dom v0) /\ Z) /\ ((dom u0) /\ (dom (y `| Z))) by A3, FDIFF_1:def 7
.= ((dom v0) /\ Z) /\ ((dom u0) /\ Z) by A3, FDIFF_1:def 7
.= (dom v0) /\ (Z /\ ((dom u0) /\ Z)) by XBOOLE_1:16
.= (dom v0) /\ ((Z /\ Z) /\ (dom u0)) by XBOOLE_1:16
.= ((dom v0) /\ (dom u0)) /\ Z by XBOOLE_1:16 ;
A46: ['a,b'] c= (dom v0) /\ (dom u0) by A19, A29, XBOOLE_1:19;
['a,b'] c= Z by A1, A3, INTEGRA5:def 3;
hence ['a,b'] c= dom ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) by A45, A46, XBOOLE_1:19; :: thesis:

end;

A47: (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) * ) = integral (f,x,y,a,d,Z) by Def2, A5;
A48: (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b)) * ) = integral (f,x,y,d,b,Z) by Def2, A5;
A49: integral (f,x,y,a,d,Z) = integral (f,x1,y1,a,d,Z1)

proof

reconsider Z3 = Z /\ Z1 as Subset of REAL ;
reconsider ZZ = Z, ZZ1 = Z1 as Subset of R^1 by TOPMETR:17;
( ZZ is open & ZZ1 is open ) by A3, A6, BORSUK_5:39;
then ZZ /\ ZZ1 is open by TOPS_1:11;
then A50: Z3 is open by BORSUK_5:39;
A51: [.a,d.] c= [.a,b.] by A2, XXREAL_1:34;
then A52: ( [.a,d.] c= dom x & [.a,d.] c= dom y ) by A3, A4;
A53: x | [.a,d.] = x1 | [.a,d.]

proof

A54: dom (x | [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3, A4, A51, XBOOLE_1:1, XBOOLE_1:28
.= (dom x1) /\ [.a,d.] by A6, A7, XBOOLE_1:28
.= dom (x1 | [.a,d.]) by RELAT_1:61 ;
for x0 being object st x0 in dom (x | [.a,d.]) holds
(x | [.a,d.]) . x0 = (x1 | [.a,d.]) . x0

proof

let x0 be object ; :: thesis:
assume A55: x0 in dom (x | [.a,d.]) ; :: thesis:
A56: dom (x | [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A51, A3, A4, XBOOLE_1:1, XBOOLE_1:28 ;
[.a,d.] c= (dom x1) /\ (dom y1) by A6, A7, XBOOLE_1:19;
then x0 in (dom x1) /\ (dom y1) by A55, A56;
then x0 in (dom x1) /\ (dom ( (#) y1)) by VALUED_1:def 5;
then A57: x0 in dom (x1 + ( (#) y1)) by VALUED_1:def 1;
[.a,d.] c= (dom x) /\ (dom y) by A52, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A55, A56;
then x0 in (dom x) /\ (dom ( (#) y)) by VALUED_1:def 5;
then A58: x0 in dom (x + ( (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A55;
A59: C . t = C1 . t by A1, A55, A56;
A60: C . t = (x + ( (#) y)) . t by A3, A4, A51, A55, A56, FUNCT_1:49;
A61: C1 . t = (x1 + ( (#) y1)) . t by A6, A7, A55, A56, FUNCT_1:49;
A62: (x1 + ( (#) y1)) . t = (x1 . t) + (( (#) y1) . t) by A57, VALUED_1:def 1
.= (x1 . t) + ( * (y1 . t)) by VALUED_1:6 ;
A63: (x + ( (#) y)) . t = (x . t) + (( (#) y) . t) by A58, VALUED_1:def 1
.= (x . t) + ( * (y . t)) by VALUED_1:6 ;
thus (x | [.a,d.]) . x0 = x . x0 by A55, FUNCT_1:47
.= x1 . x0 by A59, A60, A61, A62, A63, COMPLEX1:77
.= (x1 | [.a,d.]) . x0 by A56, A55, FUNCT_1:49 ; :: thesis:

end;

hence x | [.a,d.] = x1 | [.a,d.] by A54, FUNCT_1:2; :: thesis:

end;

A64: y | [.a,d.] = y1 | [.a,d.]

proof

A65: dom (y | [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3, A4, A51, XBOOLE_1:1, XBOOLE_1:28
.= (dom y1) /\ [.a,d.] by A6, A7, XBOOLE_1:28
.= dom (y1 | [.a,d.]) by RELAT_1:61 ;
for x0 being object st x0 in dom (y | [.a,d.]) holds
(y | [.a,d.]) . x0 = (y1 | [.a,d.]) . x0

proof

let x0 be object ; :: thesis:
assume A66: x0 in dom (y | [.a,d.]) ; :: thesis:
A67: dom (y | [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3, A4, A51, XBOOLE_1:1, XBOOLE_1:28 ;
[.a,d.] c= (dom x1) /\ (dom y1) by A6, A7, XBOOLE_1:19;
then x0 in (dom x1) /\ (dom y1) by A66, A67;
then x0 in (dom x1) /\ (dom ( (#) y1)) by VALUED_1:def 5;
then A68: x0 in dom (x1 + ( (#) y1)) by VALUED_1:def 1;
[.a,d.] c= (dom x) /\ (dom y) by A52, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A66, A67;
then x0 in (dom x) /\ (dom ( (#) y)) by VALUED_1:def 5;
then A69: x0 in dom (x + ( (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A66;
A70: C . t = C1 . t by A1, A66, A67;
A71: C . t = (x + ( (#) y)) . t by A3, A4, A51, A66, A67, FUNCT_1:49;
A72: C1 . t = (x1 + ( (#) y1)) . t by A6, A7, A66, A67, FUNCT_1:49;
A73: (x1 + ( (#) y1)) . t = (x1 . t) + (( (#) y1) . t) by A68, VALUED_1:def 1
.= (x1 . t) + ( * (y1 . t)) by VALUED_1:6 ;
A74: (x + ( (#) y)) . t = (x . t) + (( (#) y) . t) by A69, VALUED_1:def 1
.= (x . t) + ( * (y . t)) by VALUED_1:6 ;
thus (y | [.a,d.]) . x0 = y . x0 by A66, FUNCT_1:47
.= y1 . x0 by A70, A71, A72, A73, A74, COMPLEX1:77
.= (y1 | [.a,d.]) . x0 by A67, A66, FUNCT_1:49 ; :: thesis:

end;

hence y | [.a,d.] = y1 | [.a,d.] by A65, FUNCT_1:2; :: thesis:

end;

A75: [.a,d.] c= Z by A3, A4, A51;
then A76: [.a,d.] c= Z3 by A6, A7, XBOOLE_1:19;
A77: rng ((x + ( (#) y)) | [.a,d.]) c= dom f

proof

let y0 be object ; :: according to TARSKI:def 3 :: thesis:
assume A78: y0 in rng ((x + ( (#) y)) | [.a,d.]) ; :: thesis:
consider x0 being object such that
A79: ( x0 in dom ((x + ( (#) y)) | [.a,d.]) & y0 = ((x + ( (#) y)) | [.a,d.]) . x0 ) by A78, FUNCT_1:def 3;
A80: x0 in (dom (x + ( (#) y))) /\ [.a,d.] by A79, RELAT_1:61;
(dom (x + ( (#) y))) /\ [.a,d.] c= (dom (x + ( (#) y))) /\ [.a,b.] by A2, XBOOLE_1:26, XXREAL_1:34;
then x0 in (dom (x + ( (#) y))) /\ [.a,b.] by A80;
then A81: x0 in dom ((x + ( (#) y)) | [.a,b.]) by RELAT_1:61;
then A82: ((x + ( (#) y)) | [.a,b.]) . x0 in rng ((x + ( (#) y)) | [.a,b.]) by FUNCT_1:3;
((x + ( (#) y)) | [.a,d.]) . x0 = (x + ( (#) y)) . x0 by A79, FUNCT_1:47
.= ((x + ( (#) y)) | [.a,b.]) . x0 by A81, FUNCT_1:47 ;
hence y0 in dom f by A1, A3, A79, A82; :: thesis:

end;

A83: rng ((x1 + ( (#) y1)) | [.a,d.]) c= dom f

proof

let y0 be object ; :: according to TARSKI:def 3 :: thesis:
assume A84: y0 in rng ((x1 + ( (#) y1)) | [.a,d.]) ; :: thesis:
consider x0 being object such that
A85: ( x0 in dom ((x1 + ( (#) y1)) | [.a,d.]) & y0 = ((x1 + ( (#) y1)) | [.a,d.]) . x0 ) by A84, FUNCT_1:def 3;
x0 in (dom (x1 + ( (#) y1))) /\ [.a,d.] by A85, RELAT_1:61;
then A86: x0 in [.a,d.] by XBOOLE_0:def 4;
then x0 in [.a,b.] by A51;
then x0 in (dom x) /\ (dom y) by A3, A4, XBOOLE_0:def 4;
then x0 in ((dom x) /\ (dom y)) /\ [.a,b.] by A51, A86, XBOOLE_0:def 4;
then x0 in ((dom x) /\ (dom ( (#) y))) /\ [.a,b.] by VALUED_1:def 5;
then x0 in (dom (x + ( (#) y))) /\ [.a,b.] by VALUED_1:def 1;
then x0 in dom ((x + ( (#) y)) | [.a,b.]) by RELAT_1:61;
then A87: ((x + ( (#) y)) | [.a,b.]) . x0 in rng ((x + ( (#) y)) | [.a,b.]) by FUNCT_1:3;
reconsider t = x0 as Element of REAL by A85;
A88: C . t = (x + ( (#) y)) . t by A3, A4, A51, A86, FUNCT_1:49;
A89: C1 . t = (x1 + ( (#) y1)) . t by A6, A7, A86, FUNCT_1:49;
((x1 + ( (#) y1)) | [.a,d.]) . x0 = (x1 + ( (#) y1)) . x0 by A85, FUNCT_1:47
.= (x + ( (#) y)) . x0 by A1, A86, A88, A89
.= ((x + ( (#) y)) | [.a,b.]) . x0 by A51, A86, FUNCT_1:49 ;
hence y0 in dom f by A1, A3, A85, A87; :: thesis:

end;

A90: ( x is_differentiable_on Z3 & y is_differentiable_on Z3 ) by A3, A50, FDIFF_1:26, XBOOLE_1:17;
A91: ( x1 is_differentiable_on Z3 & y1 is_differentiable_on Z3 ) by A6, A50, FDIFF_1:26, XBOOLE_1:17;
A92: ( [.a,d.] c= dom x & [.a,d.] c= dom y ) by A3, A4, A51;
hence integral (f,x,y,a,d,Z) = integral (f,x,y,a,d,Z3) by A3, A6, A7, A50, A77, A76, Lm1, XBOOLE_1:17
.= integral (f,x1,y1,a,d,Z3) by A6, A7, A50, A53, A64, A75, A77, A83, A90, A91, A92, Lm2, XBOOLE_1:19
.= integral (f,x1,y1,a,d,Z1) by A6, A7, A50, A76, A83, Lm1, XBOOLE_1:17 ;
:: thesis:

end;

A93: integral (f,x,y,d,b,Z) = integral (f,x2,y2,d,b,Z2)

proof

reconsider Z3 = Z /\ Z2 as Subset of REAL ;
reconsider ZZ = Z, ZZ1 = Z2 as Subset of R^1 by TOPMETR:17;
( ZZ is open & ZZ1 is open ) by A3, A12, BORSUK_5:39;
then ZZ /\ ZZ1 is open by TOPS_1:11;
then A94: Z3 is open by BORSUK_5:39;
A95: [.d,b.] c= [.a,b.] by A2, XXREAL_1:34;
then A96: ( [.d,b.] c= dom x & [.d,b.] c= dom y ) by A3, A4;
A97: x | [.d,b.] = x2 | [.d,b.]

proof

A98: dom (x | [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A95, XBOOLE_1:1, XBOOLE_1:28
.= (dom x2) /\ [.d,b.] by A12, A13, XBOOLE_1:28
.= dom (x2 | [.d,b.]) by RELAT_1:61 ;
for x0 being object st x0 in dom (x | [.d,b.]) holds
(x | [.d,b.]) . x0 = (x2 | [.d,b.]) . x0

proof

let x0 be object ; :: thesis:
assume A99: x0 in dom (x | [.d,b.]) ; :: thesis:
A100: dom (x | [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A95, XBOOLE_1:1, XBOOLE_1:28 ;
[.d,b.] c= (dom x2) /\ (dom y2) by A12, A13, XBOOLE_1:19;
then x0 in (dom x2) /\ (dom y2) by A99, A100;
then x0 in (dom x2) /\ (dom ( (#) y2)) by VALUED_1:def 5;
then A101: x0 in dom (x2 + ( (#) y2)) by VALUED_1:def 1;
[.d,b.] c= (dom x) /\ (dom y) by A96, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A99, A100;
then x0 in (dom x) /\ (dom ( (#) y)) by VALUED_1:def 5;
then A102: x0 in dom (x + ( (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A99;
A103: C . t = C2 . t by A1, A99, A100;
A104: C . t = (x + ( (#) y)) . t by A3, A4, A95, A99, A100, FUNCT_1:49;
A105: C2 . t = (x2 + ( (#) y2)) . t by A12, A13, A99, A100, FUNCT_1:49;
A106: (x2 + ( (#) y2)) . t = (x2 . t) + (( (#) y2) . t) by A101, VALUED_1:def 1
.= (x2 . t) + ( * (y2 . t)) by VALUED_1:6 ;
A107: (x + ( (#) y)) . t = (x . t) + (( (#) y) . t) by A102, VALUED_1:def 1
.= (x . t) + ( * (y . t)) by VALUED_1:6 ;
thus (x | [.d,b.]) . x0 = x . x0 by A99, FUNCT_1:47
.= x2 . x0 by A103, A104, A105, A106, A107, COMPLEX1:77
.= (x2 | [.d,b.]) . x0 by A99, A100, FUNCT_1:49 ; :: thesis:

end;

hence x | [.d,b.] = x2 | [.d,b.] by A98, FUNCT_1:2; :: thesis:

end;

A108: y | [.d,b.] = y2 | [.d,b.]

proof

A109: dom (y | [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A95, XBOOLE_1:1, XBOOLE_1:28
.= (dom y2) /\ [.d,b.] by A12, A13, XBOOLE_1:28
.= dom (y2 | [.d,b.]) by RELAT_1:61 ;
for x0 being object st x0 in dom (y | [.d,b.]) holds
(y | [.d,b.]) . x0 = (y2 | [.d,b.]) . x0

proof

let x0 be object ; :: thesis:
assume A110: x0 in dom (y | [.d,b.]) ; :: thesis:
A111: dom (y | [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A95, XBOOLE_1:1, XBOOLE_1:28 ;
[.d,b.] c= (dom x2) /\ (dom y2) by A12, A13, XBOOLE_1:19;
then x0 in (dom x2) /\ (dom y2) by A110, A111;
then x0 in (dom x2) /\ (dom ( (#) y2)) by VALUED_1:def 5;
then A112: x0 in dom (x2 + ( (#) y2)) by VALUED_1:def 1;
[.d,b.] c= (dom x) /\ (dom y) by A96, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A110, A111;
then x0 in (dom x) /\ (dom ( (#) y)) by VALUED_1:def 5;
then A113: x0 in dom (x + ( (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A110;
A114: C . t = C2 . t by A1, A110, A111;
A115: C . t = (x + ( (#) y)) . t by A3, A4, A95, A110, A111, FUNCT_1:49;
A116: C2 . t = (x2 + ( (#) y2)) . t by A12, A13, A110, A111, FUNCT_1:49;
A117: (x2 + ( (#) y2)) . t = (x2 . t) + (( (#) y2) . t) by A112, VALUED_1:def 1
.= (x2 . t) + ( * (y2 . t)) by VALUED_1:6 ;
A118: (x + ( (#) y)) . t = (x . t) + (( (#) y) . t) by A113, VALUED_1:def 1
.= (x . t) + ( * (y . t)) by VALUED_1:6 ;
thus (y | [.d,b.]) . x0 = y . x0 by A110, FUNCT_1:47
.= y2 . x0 by A114, A115, A116, A117, A118, COMPLEX1:77
.= (y2 | [.d,b.]) . x0 by A111, A110, FUNCT_1:49 ; :: thesis:

end;

hence y | [.d,b.] = y2 | [.d,b.] by A109, FUNCT_1:2; :: thesis:

end;

A119: [.d,b.] c= Z by A3, A4, A95;
then A120: [.d,b.] c= Z3 by A12, A13, XBOOLE_1:19;
A121: rng ((x + ( (#) y)) | [.d,b.]) c= dom f

proof

end;

A127: rng ((x2 + ( (#) y2)) | [.d,b.]) c= dom f

proof

let y0 be object ; :: according to TARSKI:def 3 :: thesis:
assume A128: y0 in rng ((x2 + ( (#) y2)) | [.d,b.]) ; :: thesis:
consider x0 being object such that
A129: ( x0 in dom ((x2 + ( (#) y2)) | [.d,b.]) & y0 = ((x2 + ( (#) y2)) | [.d,b.]) . x0 ) by A128, FUNCT_1:def 3;
x0 in (dom (x2 + ( (#) y2))) /\ [.d,b.] by A129, RELAT_1:61;
then A130: x0 in [.d,b.] by XBOOLE_0:def 4;
then x0 in [.a,b.] by A95;
then x0 in (dom x) /\ (dom y) by A3, A4, XBOOLE_0:def 4;
then x0 in ((dom x) /\ (dom y)) /\ [.a,b.] by A95, A130, XBOOLE_0:def 4;
then x0 in ((dom x) /\ (dom ( (#) y))) /\ [.a,b.] by VALUED_1:def 5;
then x0 in (dom (x + ( (#) y))) /\ [.a,b.] by VALUED_1:def 1;
then x0 in dom ((x + ( (#) y)) | [.a,b.]) by RELAT_1:61;
then A131: ((x + ( (#) y)) | [.a,b.]) . x0 in rng ((x + ( (#) y)) | [.a,b.]) by FUNCT_1:3;
reconsider t = x0 as Element of REAL by A129;
A132: C . t = (x + ( (#) y)) . t by A3, A4, A95, A130, FUNCT_1:49;
A133: C2 . t = (x2 + ( (#) y2)) . t by A12, A13, A130, FUNCT_1:49;
((x2 + ( (#) y2)) | [.d,b.]) . x0 = (x2 + ( (#) y2)) . x0 by A129, FUNCT_1:47
.= (x + ( (#) y)) . x0 by A1, A130, A132, A133
.= ((x + ( (#) y)) | [.a,b.]) . x0 by A95, A130, FUNCT_1:49 ;
hence y0 in dom f by A1, A3, A129, A131; :: thesis:

end;

A134: ( x is_differentiable_on Z3 & y is_differentiable_on Z3 ) by A3, A94, FDIFF_1:26, XBOOLE_1:17;
A135: ( x2 is_differentiable_on Z3 & y2 is_differentiable_on Z3 ) by A12, A94, FDIFF_1:26, XBOOLE_1:17;
A136: ( [.d,b.] c= dom x & [.d,b.] c= dom y ) by A3, A4, A95;
hence integral (f,x,y,d,b,Z) = integral (f,x,y,d,b,Z3) by A3, A12, A13, A94, A120, A121, Lm1, XBOOLE_1:17
.= integral (f,x2,y2,d,b,Z3) by Lm2, A12, A13, A94, A97, A108, A119, A121, A127, A134, A135, A136, XBOOLE_1:19
.= integral (f,x2,y2,d,b,Z2) by A12, A13, A94, A120, A127, Lm1, XBOOLE_1:17 ;
:: thesis:

end;

thus integral (f,C) = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * ) by A1, A3, A5, Def4
.= ((integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b))) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * ) by A1, A18, A39, A40, A41, INTEGRA6:17
.= ((integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b))) + (((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) + (integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b))) * ) by A1, A18, A39, A40, A44, INTEGRA6:17
.= (integral (f,x1,y1,a,d,Z1)) + (integral (f,x,y,d,b,Z)) by A49, A48, A47
.= (integral (f,C1)) + (integral (f,C2)) by A6, A7, A8, A17, Def4, A93 ; :: thesis: