let f be PartFunc of COMPLEX,COMPLEX; :: thesis: for C, C1, C2 being C1-curve
for a, b, d being Real st 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 Element of REAL st t in dom C1 holds
C . t = C1 . t ) & ( for t being Element of REAL st t in dom C2 holds
C . t = C2 . t ) holds
integral (f,C) = (integral (f,C1)) + (integral (f,C2))
let C, C1, C2 be C1-curve; :: thesis: for a, b, d being Real st 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 Element of REAL st t in dom C1 holds
C . t = C1 . t ) & ( for t being Element of REAL st t in dom C2 holds
C . t = C2 . t ) holds
integral (f,C) = (integral (f,C1)) + (integral (f,C2))
let a, b, d be Real; :: thesis: ( 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 Element of REAL st t in dom C1 holds
C . t = C1 . t ) & ( for t being Element of REAL st t in dom C2 holds
C . t = C2 . t ) implies integral (f,C) = (integral (f,C1)) + (integral (f,C2)) )
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 Element of REAL st t in dom C1 holds
C . t = C1 . t ) & ( for t being Element of REAL st t in dom C2 holds
C . t = C2 . t ) ) ; :: thesis: integral (f,C) = (integral (f,C1)) + (integral (f,C2))
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 + (<i> (#) 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: b0 = b
thus b0 = sup [.a0,b0.] by A3, XXREAL_2:29
.= b by A1, A3, XXREAL_2:29 ; :: thesis: verum

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)) * <i>) ) 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 + (<i> (#) 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: b1 = d
thus b1 = sup [.a1,b1.] by A6, XXREAL_2:29
.= d by A2, A1, A6, XXREAL_2:29 ; :: thesis: verum

end;

A8: rng C1 c= dom f

proof

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

proof

let y0 be set ; :: thesis: ( y0 in rng C1 implies y0 in rng C )
assume A10: y0 in rng C1 ; :: thesis: y0 in rng C
consider x0 being set 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: verum

end;

then rng C1 c= rng C by TARSKI:def 3;
hence rng C1 c= dom f by A1, XBOOLE_1:1; :: thesis: verum

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 + (<i> (#) 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: b2 = b
thus b2 = sup [.a2,b2.] by A12, XXREAL_2:29
.= b by A2, A1, A12, XXREAL_2:29 ; :: thesis: verum

end;

rng C2 c= dom f

proof

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

proof

let y0 be set ; :: thesis: ( y0 in rng C2 implies y0 in rng C )
assume A15: y0 in rng C2 ; :: thesis: y0 in rng C
consider x0 being set 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: verum

end;

then rng C2 c= rng C by TARSKI:def 3;
hence rng C2 c= dom f by A1, XBOOLE_1:1; :: thesis: verum

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 set st x0 in [.a,b.] holds
x0 in dom u0

proof

let x0 be set ; :: thesis: ( x0 in [.a,b.] implies x0 in dom u0 )
assume A20: x0 in [.a,b.] ; :: thesis: x0 in dom u0
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;
<:x,y:> . x0 = [(x . x0),(y . x0)] 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 (<i> (#) y) by A22, VALUED_1:def 5;
then x0 in (dom x) /\ (dom (<i> (#) y)) by A3, A4, A20, XBOOLE_0:def 4;
then A26: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
A27: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def 2;
A28: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) by MCART_1:7;
C . x0 = (x + (<i> (#) y)) . x0 by A20, A3, A4, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A26, VALUED_1:def 1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] 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: verum

end;

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

end;

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

proof

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

proof

let x0 be set ; :: thesis: ( x0 in [.a,b.] implies x0 in dom v0 )
assume A30: x0 in [.a,b.] ; :: thesis: x0 in dom v0
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;
<:x,y:> . x0 = [(x . x0),(y . x0)] 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 (<i> (#) y) by A32, VALUED_1:def 5;
then x0 in (dom x) /\ (dom (<i> (#) y)) by A3, A4, A30, XBOOLE_0:def 4;
then A36: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
A37: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def 2;
A38: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) by MCART_1:7;
C . x0 = (x + (<i> (#) y)) . x0 by A30, A3, A4, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A36, VALUED_1:def 1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] 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: verum

end;

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

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, Def5;
A40: ( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded & ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded ) by A1, A3, Def6;
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: verum

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: verum

end;

A47: (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) * <i>) = integral (f,x,y,a,d,Z)

proof

consider u1, v1 being PartFunc of REAL,REAL such that
A48: ( u1 = ((Re f) * R2-to-C) * <:x,y:> & v1 = ((Im f) * R2-to-C) * <:x,y:> & integral (f,x,y,a,d,Z) = (integral (((u1 (#) (x `| Z)) - (v1 (#) (y `| Z))),a,d)) + ((integral (((v1 (#) (x `| Z)) + (u1 (#) (y `| Z))),a,d)) * <i>) ) by Def2;
thus (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) * <i>) = integral (f,x,y,a,d,Z) by A5, A48; :: thesis: verum

end;

A49: (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b)) * <i>) = integral (f,x,y,d,b,Z)

proof

consider u1, v1 being PartFunc of REAL,REAL such that
A50: ( u1 = ((Re f) * R2-to-C) * <:x,y:> & v1 = ((Im f) * R2-to-C) * <:x,y:> & integral (f,x,y,d,b,Z) = (integral (((u1 (#) (x `| Z)) - (v1 (#) (y `| Z))),d,b)) + ((integral (((v1 (#) (x `| Z)) + (u1 (#) (y `| Z))),d,b)) * <i>) ) by Def2;
thus (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b)) * <i>) = integral (f,x,y,d,b,Z) by A5, A50; :: thesis: verum

end;

A51: 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 A52: Z3 is open by BORSUK_5:39;
A53: [.a,d.] c= [.a,b.] by A2, XXREAL_1:34;
then A54: ( [.a,d.] c= dom x & [.a,d.] c= dom y ) by A3, A4, XBOOLE_1:1;
A55: x | [.a,d.] = x1 | [.a,d.]

proof

A56: dom (x | [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3, A4, A53, 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 set st x0 in dom (x | [.a,d.]) holds
(x | [.a,d.]) . x0 = (x1 | [.a,d.]) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (x | [.a,d.]) implies (x | [.a,d.]) . x0 = (x1 | [.a,d.]) . x0 )
assume A57: x0 in dom (x | [.a,d.]) ; :: thesis: (x | [.a,d.]) . x0 = (x1 | [.a,d.]) . x0
A58: dom (x | [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A53, 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 A57, A58;
then x0 in (dom x1) /\ (dom (<i> (#) y1)) by VALUED_1:def 5;
then A59: x0 in dom (x1 + (<i> (#) y1)) by VALUED_1:def 1;
[.a,d.] c= (dom x) /\ (dom y) by A54, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A57, A58;
then x0 in (dom x) /\ (dom (<i> (#) y)) by VALUED_1:def 5;
then A60: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A57;
A61: C . t = C1 . t by A1, A57, A58;
A62: C . t = (x + (<i> (#) y)) . t by A3, A4, A53, A57, A58, FUNCT_1:49;
A63: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A57, A58, FUNCT_1:49;
A64: (x1 + (<i> (#) y1)) . t = (x1 . t) + ((<i> (#) y1) . t) by A59, VALUED_1:def 1
.= (x1 . t) + (<i> * (y1 . t)) by VALUED_1:6 ;
A65: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A60, VALUED_1:def 1
.= (x . t) + (<i> * (y . t)) by VALUED_1:6 ;
thus (x | [.a,d.]) . x0 = x . x0 by A57, FUNCT_1:47
.= x1 . x0 by A61, A62, A63, A64, A65, COMPLEX1:77
.= (x1 | [.a,d.]) . x0 by A58, A57, FUNCT_1:49 ; :: thesis: verum

end;

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

end;

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

proof

A67: dom (y | [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3, A4, A53, 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 set st x0 in dom (y | [.a,d.]) holds
(y | [.a,d.]) . x0 = (y1 | [.a,d.]) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (y | [.a,d.]) implies (y | [.a,d.]) . x0 = (y1 | [.a,d.]) . x0 )
assume A68: x0 in dom (y | [.a,d.]) ; :: thesis: (y | [.a,d.]) . x0 = (y1 | [.a,d.]) . x0
A69: dom (y | [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3, A4, A53, 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 A68, A69;
then x0 in (dom x1) /\ (dom (<i> (#) y1)) by VALUED_1:def 5;
then A70: x0 in dom (x1 + (<i> (#) y1)) by VALUED_1:def 1;
[.a,d.] c= (dom x) /\ (dom y) by A54, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A68, A69;
then x0 in (dom x) /\ (dom (<i> (#) y)) by VALUED_1:def 5;
then A71: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A68;
A72: C . t = C1 . t by A1, A68, A69;
A73: C . t = (x + (<i> (#) y)) . t by A3, A4, A53, A68, A69, FUNCT_1:49;
A74: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A68, A69, FUNCT_1:49;
A75: (x1 + (<i> (#) y1)) . t = (x1 . t) + ((<i> (#) y1) . t) by A70, VALUED_1:def 1
.= (x1 . t) + (<i> * (y1 . t)) by VALUED_1:6 ;
A76: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A71, VALUED_1:def 1
.= (x . t) + (<i> * (y . t)) by VALUED_1:6 ;
thus (y | [.a,d.]) . x0 = y . x0 by A68, FUNCT_1:47
.= y1 . x0 by A72, A73, A74, A75, A76, COMPLEX1:77
.= (y1 | [.a,d.]) . x0 by A69, A68, FUNCT_1:49 ; :: thesis: verum

end;

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

end;

A77: [.a,d.] c= Z by A3, A4, A53, XBOOLE_1:1;
then A78: [.a,d.] c= Z3 by A6, A7, XBOOLE_1:19;
A79: rng ((x + (<i> (#) y)) | [.a,d.]) c= dom f

proof

for y0 being set st y0 in rng ((x + (<i> (#) y)) | [.a,d.]) holds
y0 in dom f

proof

let y0 be set ; :: thesis: ( y0 in rng ((x + (<i> (#) y)) | [.a,d.]) implies y0 in dom f )
assume A80: y0 in rng ((x + (<i> (#) y)) | [.a,d.]) ; :: thesis: y0 in dom f
consider x0 being set such that
A81: ( x0 in dom ((x + (<i> (#) y)) | [.a,d.]) & y0 = ((x + (<i> (#) y)) | [.a,d.]) . x0 ) by A80, FUNCT_1:def 3;
A82: x0 in (dom (x + (<i> (#) y))) /\ [.a,d.] by A81, RELAT_1:61;
(dom (x + (<i> (#) y))) /\ [.a,d.] c= (dom (x + (<i> (#) y))) /\ [.a,b.] by A2, XBOOLE_1:26, XXREAL_1:34;
then x0 in (dom (x + (<i> (#) y))) /\ [.a,b.] by A82;
then A83: x0 in dom ((x + (<i> (#) y)) | [.a,b.]) by RELAT_1:61;
then A84: ((x + (<i> (#) y)) | [.a,b.]) . x0 in rng ((x + (<i> (#) y)) | [.a,b.]) by FUNCT_1:3;
((x + (<i> (#) y)) | [.a,d.]) . x0 = (x + (<i> (#) y)) . x0 by A81, FUNCT_1:47
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A83, FUNCT_1:47 ;
hence y0 in dom f by A1, A3, A81, A84; :: thesis: verum

end;

hence rng ((x + (<i> (#) y)) | [.a,d.]) c= dom f by TARSKI:def 3; :: thesis: verum

end;

A85: rng ((x1 + (<i> (#) y1)) | [.a,d.]) c= dom f

proof

for y0 being set st y0 in rng ((x1 + (<i> (#) y1)) | [.a,d.]) holds
y0 in dom f

proof

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

end;

hence rng ((x1 + (<i> (#) y1)) | [.a,d.]) c= dom f by TARSKI:def 3; :: thesis: verum

end;

A92: ( x is_differentiable_on Z3 & y is_differentiable_on Z3 ) by A3, A52, FDIFF_1:26, XBOOLE_1:17;
A93: ( x1 is_differentiable_on Z3 & y1 is_differentiable_on Z3 ) by A6, A52, FDIFF_1:26, XBOOLE_1:17;
A94: ( [.a,d.] c= dom x & [.a,d.] c= dom y ) by A3, A4, A53, XBOOLE_1:1;
hence integral (f,x,y,a,d,Z) = integral (f,x,y,a,d,Z3) by A3, A6, A7, A52, A79, A78, Lm1, XBOOLE_1:17
.= integral (f,x1,y1,a,d,Z3) by A6, A7, A52, A55, A66, A77, A79, A85, A92, A93, A94, Lm2, XBOOLE_1:19
.= integral (f,x1,y1,a,d,Z1) by A6, A7, A52, A78, A85, Lm1, XBOOLE_1:17 ;
:: thesis: verum

end;

A95: 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 A96: Z3 is open by BORSUK_5:39;
A97: [.d,b.] c= [.a,b.] by A2, XXREAL_1:34;
then A98: ( [.d,b.] c= dom x & [.d,b.] c= dom y ) by A3, A4, XBOOLE_1:1;
A99: x | [.d,b.] = x2 | [.d,b.]

proof

A100: dom (x | [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A97, 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 set st x0 in dom (x | [.d,b.]) holds
(x | [.d,b.]) . x0 = (x2 | [.d,b.]) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (x | [.d,b.]) implies (x | [.d,b.]) . x0 = (x2 | [.d,b.]) . x0 )
assume A101: x0 in dom (x | [.d,b.]) ; :: thesis: (x | [.d,b.]) . x0 = (x2 | [.d,b.]) . x0
A102: dom (x | [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A97, 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 A101, A102;
then x0 in (dom x2) /\ (dom (<i> (#) y2)) by VALUED_1:def 5;
then A103: x0 in dom (x2 + (<i> (#) y2)) by VALUED_1:def 1;
[.d,b.] c= (dom x) /\ (dom y) by A98, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A101, A102;
then x0 in (dom x) /\ (dom (<i> (#) y)) by VALUED_1:def 5;
then A104: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A101;
A105: C . t = C2 . t by A1, A101, A102;
A106: C . t = (x + (<i> (#) y)) . t by A3, A4, A97, A101, A102, FUNCT_1:49;
A107: C2 . t = (x2 + (<i> (#) y2)) . t by A12, A13, A101, A102, FUNCT_1:49;
A108: (x2 + (<i> (#) y2)) . t = (x2 . t) + ((<i> (#) y2) . t) by A103, VALUED_1:def 1
.= (x2 . t) + (<i> * (y2 . t)) by VALUED_1:6 ;
A109: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A104, VALUED_1:def 1
.= (x . t) + (<i> * (y . t)) by VALUED_1:6 ;
thus (x | [.d,b.]) . x0 = x . x0 by A101, FUNCT_1:47
.= x2 . x0 by A105, A106, A107, A108, A109, COMPLEX1:77
.= (x2 | [.d,b.]) . x0 by A101, A102, FUNCT_1:49 ; :: thesis: verum

end;

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

end;

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

proof

A111: dom (y | [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A97, 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 set st x0 in dom (y | [.d,b.]) holds
(y | [.d,b.]) . x0 = (y2 | [.d,b.]) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (y | [.d,b.]) implies (y | [.d,b.]) . x0 = (y2 | [.d,b.]) . x0 )
assume A112: x0 in dom (y | [.d,b.]) ; :: thesis: (y | [.d,b.]) . x0 = (y2 | [.d,b.]) . x0
A113: dom (y | [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3, A4, A97, 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 A112, A113;
then x0 in (dom x2) /\ (dom (<i> (#) y2)) by VALUED_1:def 5;
then A114: x0 in dom (x2 + (<i> (#) y2)) by VALUED_1:def 1;
[.d,b.] c= (dom x) /\ (dom y) by A98, XBOOLE_1:19;
then x0 in (dom x) /\ (dom y) by A112, A113;
then x0 in (dom x) /\ (dom (<i> (#) y)) by VALUED_1:def 5;
then A115: x0 in dom (x + (<i> (#) y)) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A112;
A116: C . t = C2 . t by A1, A112, A113;
A117: C . t = (x + (<i> (#) y)) . t by A3, A4, A97, A112, A113, FUNCT_1:49;
A118: C2 . t = (x2 + (<i> (#) y2)) . t by A12, A13, A112, A113, FUNCT_1:49;
A119: (x2 + (<i> (#) y2)) . t = (x2 . t) + ((<i> (#) y2) . t) by A114, VALUED_1:def 1
.= (x2 . t) + (<i> * (y2 . t)) by VALUED_1:6 ;
A120: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A115, VALUED_1:def 1
.= (x . t) + (<i> * (y . t)) by VALUED_1:6 ;
thus (y | [.d,b.]) . x0 = y . x0 by A112, FUNCT_1:47
.= y2 . x0 by A116, A117, A118, A119, A120, COMPLEX1:77
.= (y2 | [.d,b.]) . x0 by A113, A112, FUNCT_1:49 ; :: thesis: verum

end;

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

end;

A121: [.d,b.] c= Z by A3, A4, A97, XBOOLE_1:1;
then A122: [.d,b.] c= Z3 by A12, A13, XBOOLE_1:19;
A123: rng ((x + (<i> (#) y)) | [.d,b.]) c= dom f

proof

for y0 being set st y0 in rng ((x + (<i> (#) y)) | [.d,b.]) holds
y0 in dom f

proof

let y0 be set ; :: thesis: ( y0 in rng ((x + (<i> (#) y)) | [.d,b.]) implies y0 in dom f )
assume A124: y0 in rng ((x + (<i> (#) y)) | [.d,b.]) ; :: thesis: y0 in dom f
consider x0 being set such that
A125: ( x0 in dom ((x + (<i> (#) y)) | [.d,b.]) & y0 = ((x + (<i> (#) y)) | [.d,b.]) . x0 ) by A124, FUNCT_1:def 3;
A126: x0 in (dom (x + (<i> (#) y))) /\ [.d,b.] by A125, RELAT_1:61;
(dom (x + (<i> (#) y))) /\ [.d,b.] c= (dom (x + (<i> (#) y))) /\ [.a,b.] by A2, XBOOLE_1:26, XXREAL_1:34;
then x0 in (dom (x + (<i> (#) y))) /\ [.a,b.] by A126;
then A127: x0 in dom ((x + (<i> (#) y)) | [.a,b.]) by RELAT_1:61;
then A128: ((x + (<i> (#) y)) | [.a,b.]) . x0 in rng ((x + (<i> (#) y)) | [.a,b.]) by FUNCT_1:3;
((x + (<i> (#) y)) | [.d,b.]) . x0 = (x + (<i> (#) y)) . x0 by A125, FUNCT_1:47
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A127, FUNCT_1:47 ;
hence y0 in dom f by A1, A3, A125, A128; :: thesis: verum

end;

hence rng ((x + (<i> (#) y)) | [.d,b.]) c= dom f by TARSKI:def 3; :: thesis: verum

end;

A129: rng ((x2 + (<i> (#) y2)) | [.d,b.]) c= dom f

proof

for y0 being set st y0 in rng ((x2 + (<i> (#) y2)) | [.d,b.]) holds
y0 in dom f

proof

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

end;

hence rng ((x2 + (<i> (#) y2)) | [.d,b.]) c= dom f by TARSKI:def 3; :: thesis: verum

end;

A136: ( x is_differentiable_on Z3 & y is_differentiable_on Z3 ) by A3, A96, FDIFF_1:26, XBOOLE_1:17;
A137: ( x2 is_differentiable_on Z3 & y2 is_differentiable_on Z3 ) by A12, A96, FDIFF_1:26, XBOOLE_1:17;
A138: ( [.d,b.] c= dom x & [.d,b.] c= dom y ) by A3, A4, A97, XBOOLE_1:1;
hence integral (f,x,y,d,b,Z) = integral (f,x,y,d,b,Z3) by A3, A12, A13, A96, A122, A123, Lm1, XBOOLE_1:17
.= integral (f,x2,y2,d,b,Z3) by Lm2, A12, A13, A96, A99, A110, A121, A123, A129, A136, A137, A138, XBOOLE_1:19
.= integral (f,x2,y2,d,b,Z2) by A12, A13, A96, A122, A129, Lm1, XBOOLE_1:17 ;
:: thesis: verum

end;

thus integral (f,C) = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) 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)) * <i>) 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))) * <i>) by A1, A18, A39, A40, A44, INTEGRA6:17
.= (integral (f,x1,y1,a,d,Z1)) + (integral (f,x,y,d,b,Z)) by A51, A49, A47
.= (integral (f,C1)) + (integral (f,C2)) by A6, A7, A8, A17, Def4, A95 ; :: thesis: verum