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, XXREAL_2:25, A3 ; :: thesis: b0 = b
thus b0 = sup [.a0,b0.] by A3, XXREAL_2:29
.= b by A1, XXREAL_2:29, A3 ; :: 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, XXREAL_2:25, A1, A6 ; :: thesis: b1 = d
thus b1 = sup [.a1,b1.] by A6, XXREAL_2:29
.= d by A2, XXREAL_2:29, A1, A6 ; :: 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 5;
C1 . x0 = C . x0 by A1, A11;
hence y0 in rng C by A1, A9, A11, FUNCT_1:12; :: 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, XXREAL_2:25, A1, A12 ; :: thesis: b2 = b
thus b2 = sup [.a2,b2.] by A12, XXREAL_2:29
.= b by A2, XXREAL_2:29, A1, A12 ; :: 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 5;
C2 . x0 = C . x0 by A1, A16;
hence y0 in rng C by A1, A14, A16, FUNCT_1:12; :: 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 4;
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:12;
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 8;
set R2 = <:x,y:> . x0;
<:x,y:> . x0 = [(x . x0),(y . x0)] by A23, FUNCT_3:68;
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, FUNCT_1:72, A3, A4
.= (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:68 ;
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:21;
hence x0 in dom u0 by A5, A24, FUNCT_1:21; :: 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:12;
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 8;
set R2 = <:x,y:> . x0;
<:x,y:> . x0 = [(x . x0),(y . x0)] by A33, FUNCT_3:68;
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, FUNCT_1:72, A3, A4
.= (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:68 ;
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:21;
hence x0 in dom v0 by A5, A34, FUNCT_1:21; :: 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 8
.= ((dom u0) /\ Z) /\ ((dom v0) /\ Z) by A3, FDIFF_1:def 8
.= (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 4;
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 8
.= ((dom v0) /\ Z) /\ ((dom u0) /\ Z) by A3, FDIFF_1:def 8
.= (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 4;
hence ['a,b'] c= dom ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) by A45, A46, XBOOLE_1:19; :: thesis: verum

end;

reconsider AD = [.a,d.] as closed-interval Subset of REAL by A6, A7, INTEGRA1:def 1;
reconsider DB = [.d,b.] as closed-interval Subset of REAL by A12, A13, INTEGRA1:def 1;
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, ZZ3 = Z3 as Subset of R^1 by TOPMETR:24;
( ZZ is open & ZZ1 is open ) by A3, A6, BORSUK_5:62;
then ZZ /\ ZZ1 is open by TOPS_1:38;
then A52: Z3 is open by BORSUK_5:62;
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:90
.= [.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:90 ;
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:90
.= [.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:72;
A63: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A57, A58, FUNCT_1:72;
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:70
.= x1 . x0 by A61, A62, A63, A64, A65, COMPLEX1:163
.= (x1 | [.a,d.]) . x0 by A58, A57, FUNCT_1:72 ; :: thesis: verum

end;

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

end;

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

proof

A67: dom (y | [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:90
.= [.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:90 ;
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:90
.= [.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:72;
A74: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A68, A69, FUNCT_1:72;
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:70
.= y1 . x0 by A72, A73, A74, A75, A76, COMPLEX1:163
.= (y1 | [.a,d.]) . x0 by A69, A68, FUNCT_1:72 ; :: thesis: verum

end;

hence y | [.a,d.] = y1 | [.a,d.] by A67, FUNCT_1:9; :: 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 5;
A82: x0 in (dom (x + (<i> (#) y))) /\ [.a,d.] by A81, RELAT_1:90;
(dom (x + (<i> (#) y))) /\ [.a,d.] c= (dom (x + (<i> (#) y))) /\ [.a,b.] by A2, XXREAL_1:34, XBOOLE_1:26;
then x0 in (dom (x + (<i> (#) y))) /\ [.a,b.] by A82;
then A83: x0 in dom ((x + (<i> (#) y)) | [.a,b.]) by RELAT_1:90;
then A84: ((x + (<i> (#) y)) | [.a,b.]) . x0 in rng ((x + (<i> (#) y)) | [.a,b.]) by FUNCT_1:12;
((x + (<i> (#) y)) | [.a,d.]) . x0 = (x + (<i> (#) y)) . x0 by A81, FUNCT_1:70
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A83, FUNCT_1:70 ;
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 5;
x0 in (dom (x1 + (<i> (#) y1))) /\ [.a,d.] by A87, RELAT_1:90;
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:90;
then A90: ((x + (<i> (#) y)) | [.a,b.]) . x0 in rng ((x + (<i> (#) y)) | [.a,b.]) by FUNCT_1:12;
reconsider t = x0 as Element of REAL by A87;
A91: C . t = (x + (<i> (#) y)) . t by A3, A4, A53, A88, FUNCT_1:72;
A92: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A88, FUNCT_1:72;
((x1 + (<i> (#) y1)) | [.a,d.]) . x0 = (x1 + (<i> (#) y1)) . x0 by A87, FUNCT_1:70
.= (x + (<i> (#) y)) . x0 by A1, A88, A91, A92
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A53, A88, FUNCT_1:72 ;
hence y0 in dom f by A1, A3, A87, A90; :: thesis: verum

end;

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

end;

A93: ( x is_differentiable_on Z3 & y is_differentiable_on Z3 ) by A3, A52, XBOOLE_1:17, FDIFF_1:34;
A94: ( x1 is_differentiable_on Z3 & y1 is_differentiable_on Z3 ) by A6, A52, XBOOLE_1:17, FDIFF_1:34;
A95: ( [.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, A93, A94, A95, Lm2, XBOOLE_1:19
.= integral f,x1,y1,a,d,Z1 by A6, A7, A52, A78, A85, Lm1, XBOOLE_1:17 ;
:: thesis: verum

end;

A96: 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, ZZ3 = Z3 as Subset of R^1 by TOPMETR:24;
( ZZ is open & ZZ1 is open ) by A3, A12, BORSUK_5:62;
then ZZ /\ ZZ1 is open by TOPS_1:38;
then A97: Z3 is open by BORSUK_5:62;
A98: [.d,b.] c= [.a,b.] by A2, XXREAL_1:34;
then A99: ( [.d,b.] c= dom x & [.d,b.] c= dom y ) by A3, A4, XBOOLE_1:1;
A100: x | [.d,b.] = x2 | [.d,b.]

proof

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

end;

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

end;

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

proof

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

end;

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

end;

A122: [.d,b.] c= Z by A3, A4, A98, XBOOLE_1:1;
then A123: [.d,b.] c= Z3 by A12, A13, XBOOLE_1:19;
A124: 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 A125: y0 in rng ((x + (<i> (#) y)) | [.d,b.]) ; :: thesis: y0 in dom f
consider x0 being set such that
A126: ( x0 in dom ((x + (<i> (#) y)) | [.d,b.]) & y0 = ((x + (<i> (#) y)) | [.d,b.]) . x0 ) by A125, FUNCT_1:def 5;
A127: x0 in (dom (x + (<i> (#) y))) /\ [.d,b.] by A126, RELAT_1:90;
(dom (x + (<i> (#) y))) /\ [.d,b.] c= (dom (x + (<i> (#) y))) /\ [.a,b.] by A2, XXREAL_1:34, XBOOLE_1:26;
then x0 in (dom (x + (<i> (#) y))) /\ [.a,b.] by A127;
then A128: x0 in dom ((x + (<i> (#) y)) | [.a,b.]) by RELAT_1:90;
then A129: ((x + (<i> (#) y)) | [.a,b.]) . x0 in rng ((x + (<i> (#) y)) | [.a,b.]) by FUNCT_1:12;
((x + (<i> (#) y)) | [.d,b.]) . x0 = (x + (<i> (#) y)) . x0 by A126, FUNCT_1:70
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A128, FUNCT_1:70 ;
hence y0 in dom f by A1, A3, A126, A129; :: thesis: verum

end;

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

end;

A130: 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 A131: y0 in rng ((x2 + (<i> (#) y2)) | [.d,b.]) ; :: thesis: y0 in dom f
consider x0 being set such that
A132: ( x0 in dom ((x2 + (<i> (#) y2)) | [.d,b.]) & y0 = ((x2 + (<i> (#) y2)) | [.d,b.]) . x0 ) by A131, FUNCT_1:def 5;
x0 in (dom (x2 + (<i> (#) y2))) /\ [.d,b.] by A132, RELAT_1:90;
then A133: x0 in [.d,b.] by XBOOLE_0:def 4;
then x0 in [.a,b.] by A98;
then x0 in (dom x) /\ (dom y) by A3, A4, XBOOLE_0:def 4;
then x0 in ((dom x) /\ (dom y)) /\ [.a,b.] by A98, A133, 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:90;
then A135: ((x + (<i> (#) y)) | [.a,b.]) . x0 in rng ((x + (<i> (#) y)) | [.a,b.]) by FUNCT_1:12;
reconsider t = x0 as Element of REAL by A132;
A136: C . t = (x + (<i> (#) y)) . t by A3, A4, A98, A133, FUNCT_1:72;
A137: C2 . t = (x2 + (<i> (#) y2)) . t by A12, A13, A133, FUNCT_1:72;
((x2 + (<i> (#) y2)) | [.d,b.]) . x0 = (x2 + (<i> (#) y2)) . x0 by A132, FUNCT_1:70
.= (x + (<i> (#) y)) . x0 by A1, A133, A136, A137
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A98, A133, FUNCT_1:72 ;
hence y0 in dom f by A1, A3, A132, A135; :: thesis: verum

end;

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

end;

A138: ( x is_differentiable_on Z3 & y is_differentiable_on Z3 ) by A3, A97, XBOOLE_1:17, FDIFF_1:34;
A139: ( x2 is_differentiable_on Z3 & y2 is_differentiable_on Z3 ) by A12, A97, XBOOLE_1:17, FDIFF_1:34;
A140: ( [.d,b.] c= dom x & [.d,b.] c= dom y ) by A3, A4, A98, XBOOLE_1:1;
hence integral f,x,y,d,b,Z = integral f,x,y,d,b,Z3 by A3, A12, A13, A97, A123, A124, Lm1, XBOOLE_1:17
.= integral f,x2,y2,d,b,Z3 by Lm2, A12, A13, A97, A100, A111, A122, A124, A130, A138, A139, A140, XBOOLE_1:19
.= integral f,x2,y2,d,b,Z2 by A12, A13, A97, A123, A130, 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, A96 ; :: thesis: verum