:: INTEGR1C semantic presentation

begin


definition
func R2-to-C  ->  Function of [:REAL,REAL:],COMPLEX means :Def1: :: INTEGR1C:def 1
 for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
it . [a,b] = a + (b * <i>);
existence
 ex b1 being Function of [:REAL,REAL:],COMPLEX st
for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b1 . [a,b] = a + (b * <i>)
proof
deffunc H1( Element of REAL , Element of REAL ) ->  set = $1 + ($2 * <i>);
A1: for x, y being Element of REAL holds H1(x,y) in COMPLEX by XCMPLX_0:def_2;
consider f being Function of [:REAL,REAL:],COMPLEX such that
A2: for x, y being Element of REAL holds f . (x,y) = H1(x,y) from FUNCT_7:sch_1(A1);
deffunc H2( Element of [:REAL,REAL:]) ->  set = f . (($1 `1),($1 `2));
A3: now__::_thesis:_for_p_being_Element_of_[:REAL,REAL:]_holds_H2(p)_in_COMPLEX
let p be Element of [:REAL,REAL:]; ::_thesis: H2(p) in COMPLEX
 ( p `1 is Element of REAL & p `2 is Element of REAL ) by MCART_1:10;
then consider a, b being Element of REAL  such that
A4: ( a = p `1 & b = p `2 ) ;
 H2(p) = a + (b * <i>) by A2, A4;
hence  H2(p) in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
consider g being Function of [:REAL,REAL:],COMPLEX such that
A5: for p being Element of [:REAL,REAL:] holds g . p = H2(p) from FUNCT_2:sch_8(A3);
take  g ; ::_thesis: for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>)
 for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>)
proof
let p be Element of [:REAL,REAL:]; ::_thesis: for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>)
let a, b be Element of REAL ; ::_thesis: ( a = p `1 & b = p `2 implies g . [a,b] = a + (b * <i>) )
assume A6: ( a = p `1 & b = p `2 ) ; ::_thesis: g . [a,b] = a + (b * <i>)
A7: [a,b] `1 is Element of REAL ;
 [a,b] `2 is Element of REAL ;
then A8: [a,b] is Element of [:REAL,REAL:] by A7, MCART_1:11;
A9: [a,b] `1 = p `1 by A6;
 [a,b] `2 = p `2 by A6;
then g . [a,b] = f . (a,b) by A5, A8, A9
.= a + (b * <i>) by A2 ;
hence  g . [a,b] = a + (b * <i>) ; ::_thesis: verum
end;
hence  for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:REAL,REAL:],COMPLEX st ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b1 . [a,b] = a + (b * <i>) ) & ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b2 . [a,b] = a + (b * <i>) ) holds
b1 = b2
proof
let f, g be Function of [:REAL,REAL:],COMPLEX; ::_thesis: ( ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
f . [a,b] = a + (b * <i>) ) & ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>) ) implies f = g )
assume A10: for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
f . [a,b] = a + (b * <i>) ; ::_thesis: ( ex p being Element of [:REAL,REAL:] ex a, b being Element of REAL st
( a = p `1 & b = p `2 & not g . [a,b] = a + (b * <i>) ) or f = g )
assume A11: for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>) ; ::_thesis: f = g
 for p0 being set st p0 in [:REAL,REAL:] holds
f . p0 = g . p0
proof
let p0 be set ; ::_thesis: ( p0 in [:REAL,REAL:] implies f . p0 = g . p0 )
assume A12: p0 in [:REAL,REAL:] ; ::_thesis: f . p0 = g . p0
then consider x0, y0 being set  such that
A13: ( x0 in REAL & y0 in REAL & p0 = [x0,y0] ) by ZFMISC_1:def_2;
reconsider a = x0, b = y0 as Element of REAL by A13;
A14: p0 `1 = a by A13, MCART_1:7;
A15: p0 `2 = b by A13, MCART_1:7;
then f . p0 = a + (b * <i>) by A12, A10, A14, A13
.= g . p0 by A13, A12, A11, A14, A15 ;
hence  f . p0 = g . p0 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines R2-to-C INTEGR1C:def_1_:_
 for b1 being Function of [:REAL,REAL:],COMPLEX holds
( b1 = R2-to-C iff for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
b1 . [a,b] = a + (b * <i>) );

definition
let a, b be Real;
let x, y be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let f be PartFunc of COMPLEX,COMPLEX;
func integral (f,x,y,a,b,Z) ->  Complex means :Def2: :: INTEGR1C:def 2
 ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & it = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) );
existence
 ex b1 being Complex ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) )
proof
A1: dom <:x,y:> = (dom x) /\ (dom y) by FUNCT_3:def_7;
 rng <:x,y:> c= [:(rng x),(rng y):] by FUNCT_3:51;
then  rng <:x,y:> c= [:REAL,REAL:] by XBOOLE_1:1;
then reconsider xy = <:x,y:> as PartFunc of REAL,[:REAL,REAL:] by A1, RELSET_1:4;
 ((Re f) * R2-to-C) * xy is PartFunc of REAL,REAL ;
then reconsider u0 = ((Re f) * R2-to-C) * <:x,y:> as PartFunc of REAL,REAL ;
 ((Im f) * R2-to-C) * xy is PartFunc of REAL,REAL ;
then reconsider v0 = ((Im f) * R2-to-C) * <:x,y:> as PartFunc of REAL,REAL ;
 (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) is Complex ;
hence  ex b1 being Complex ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Complex st ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) & ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b2 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines integral INTEGR1C:def_2_:_
 for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for f being PartFunc of COMPLEX,COMPLEX
for b7 being Complex holds
( b7 = integral (f,x,y,a,b,Z) iff ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b7 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) );

definition
let C be PartFunc of REAL,COMPLEX;
attrC is C1-curve-like  means :Def3: :: INTEGR1C:def 3
 ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] );
end;

:: deftheorem Def3 defines C1-curve-like INTEGR1C:def_3_:_
 for C being PartFunc of REAL,COMPLEX holds
( C is C1-curve-like iff ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] ) );

registration
cluster Relation-like REAL -defined COMPLEX -valued Function-like complex-valued C1-curve-like for Element of bool [:REAL,COMPLEX:];
existence
 ex b1 being PartFunc of REAL,COMPLEX st b1 is C1-curve-like
proof
set a = 1;
set b = 2;
set x = cos ;
set y = sin ;
set Z = ].(- 5),5.[;
consider C being PartFunc of REAL,COMPLEX such that
A1: C = (cos + (<i> (#) sin)) | [.1,2.] ;
take  C ; ::_thesis: C is C1-curve-like
A2: dom (cos + (<i> (#) sin)) = REAL by FUNCT_2:def_1;
 dom C = (dom (cos + (<i> (#) sin))) /\ [.1,2.] by A1, RELAT_1:61;
then A3: [.1,2.] = dom C by A2, XBOOLE_1:28;
A4: ].(- 5),5.[ is open by RCOMP_1:7;
A5: [.1,2.] c= ].(- 5),5.[ by XXREAL_1:47;
A6: cos is_differentiable_on ].(- 5),5.[ by A4, FDIFF_1:26, SIN_COS:67;
A7: sin is_differentiable_on ].(- 5),5.[ by A4, FDIFF_1:26, SIN_COS:68;
 sin = sin | REAL
proof
thus  sin = sin | REAL ; ::_thesis: verum
end;
then  sin | ].(- 5),5.[ is continuous by FCONT_1:16;
then  (- sin) | ].(- 5),5.[ is continuous by FCONT_1:21, SIN_COS:24;
then A8: - (sin | ].(- 5),5.[) is continuous by RFUNCT_1:46;
A9: dom (- (sin | ].(- 5),5.[)) = dom ((- sin) | ].(- 5),5.[) by RFUNCT_1:46
.= (dom (- sin)) /\ ].(- 5),5.[ by RELAT_1:61
.= REAL /\ ].(- 5),5.[ by SIN_COS:24, VALUED_1:8
.= ].(- 5),5.[ by XBOOLE_1:28 ;
 for x1 being Element of REAL st x1 in ].(- 5),5.[ holds
(- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1)
proof
let x1 be Element of REAL ; ::_thesis: ( x1 in ].(- 5),5.[ implies (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1) )
assume A10: x1 in ].(- 5),5.[ ; ::_thesis: (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1)
A11: (- (sin | ].(- 5),5.[)) . x1 = ((- sin) | ].(- 5),5.[) . x1 by RFUNCT_1:46
.= (- sin) . x1 by A10, FUNCT_1:49
.= - (sin . x1) by RFUNCT_1:58
.= - ((sin | ].(- 5),5.[) . x1) by A10, FUNCT_1:49 ;
diff (cos,x1) = - (sin . x1) by SIN_COS:67
.= (- (sin | ].(- 5),5.[)) . x1 by A11, A10, FUNCT_1:49 ;
hence  (- (sin | ].(- 5),5.[)) . x1 = diff (cos,x1) ; ::_thesis: verum
end;
then A12: cos `| ].(- 5),5.[ is continuous by A6, A8, A9, FDIFF_1:def_7;
 cos = cos | REAL
proof
thus  cos = cos | REAL ; ::_thesis: verum
end;
then A13: cos | ].(- 5),5.[ is continuous by FCONT_1:16;
A14: dom (cos | ].(- 5),5.[) = (dom cos) /\ ].(- 5),5.[ by RELAT_1:61
.= ].(- 5),5.[ by SIN_COS:24, XBOOLE_1:28 ;
 for x1 being Element of REAL st x1 in ].(- 5),5.[ holds
(cos | ].(- 5),5.[) . x1 = diff (sin,x1)
proof
let x1 be Element of REAL ; ::_thesis: ( x1 in ].(- 5),5.[ implies (cos | ].(- 5),5.[) . x1 = diff (sin,x1) )
assume A15: x1 in ].(- 5),5.[ ; ::_thesis: (cos | ].(- 5),5.[) . x1 = diff (sin,x1)
diff (sin,x1) = cos . x1 by SIN_COS:68
.= (cos | ].(- 5),5.[) . x1 by A15, FUNCT_1:49 ;
hence  (cos | ].(- 5),5.[) . x1 = diff (sin,x1) ; ::_thesis: verum
end;
then  sin `| ].(- 5),5.[ is continuous by A7, A13, A14, FDIFF_1:def_7;
hence  C is C1-curve-like by A1, A3, A4, A5, A6, A7, A12, Def3, SIN_COS:24; ::_thesis: verum
end;
end;

definition
mode C1-curve is C1-curve-like PartFunc of REAL,COMPLEX;
end;

Lm1:  for a, b being Real
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)
proof
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 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: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 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 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
end;

Lm2:  for a, b being Real
for x1, y1, x2, y2 being PartFunc of REAL,REAL
for Z being Subset of REAL
for f being PartFunc of COMPLEX,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
proof
let a, b be Real; ::_thesis: for x1, y1, x2, y2 being PartFunc of REAL,REAL
for Z being Subset of REAL
for f being PartFunc of COMPLEX,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
let x1, y1, x2, y2 be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
for f being PartFunc of COMPLEX,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
let Z be Subset of REAL; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f implies integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z) )
assume A1: ( a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f ) ; ::_thesis: integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
consider u01, v01 being PartFunc of REAL,REAL such that
A2: ( u01 = ((Re f) * R2-to-C) * <:x1,y1:> & v01 = ((Im f) * R2-to-C) * <:x1,y1:> & integral (f,x1,y1,a,b,Z) = (integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b)) + ((integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b)) * <i>) ) by Def2;
consider u02, v02 being PartFunc of REAL,REAL such that
A3: ( u02 = ((Re f) * R2-to-C) * <:x2,y2:> & v02 = ((Im f) * R2-to-C) * <:x2,y2:> & integral (f,x2,y2,a,b,Z) = (integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b)) + ((integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b)) * <i>) ) by Def2;
reconsider AB = [.a,b.] as non empty closed_interval Subset of REAL by A1, MEASURE5:14;
A4: now__::_thesis:_(_a_=_b_or_a_<_b_)
assume A5: ( not a = b & not a < b ) ; ::_thesis: contradiction
then  ( 0 < b - a or 0 < a - b ) by XREAL_1:55;
then  ( a < a + (b - a) or 0 < a - b ) by XREAL_1:29;
then  ( a < b or b < b + (a - b) ) by XREAL_1:29;
hence  contradiction by A5, A1; ::_thesis: verum
end;
percases ( a < b or a = b ) by A4;
supposeA6: a < b ; ::_thesis: integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
A7: u01 | AB = u02 | AB
proof
A8: dom (u01 | AB) = dom (u02 | AB)
proof
A9: for x0 being set st x0 in dom (u01 | AB) holds
x0 in dom (u02 | AB)
proof
let x0 be set ; ::_thesis: ( x0 in dom (u01 | AB) implies x0 in dom (u02 | AB) )
assume A10: x0 in dom (u01 | AB) ; ::_thesis: x0 in dom (u02 | AB)
 x0 in (dom u01) /\ AB by A10, RELAT_1:61;
then A11: ( x0 in dom u01 & x0 in AB ) by XBOOLE_0:def_4;
then  ( x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Re f) * R2-to-C) & x0 in AB ) by A2, FUNCT_1:11;
then  ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_3:def_7;
then  ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then  ( x0 in AB & [((x2 | AB) . x0),((y2 | AB) . x0)] in dom ((Re f) * R2-to-C) ) by A1, FUNCT_1:49;
then  ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then A12: ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
 x0 in (dom x2) /\ (dom y2) by A1, A11, XBOOLE_0:def_4;
then  x0 in dom <:x2,y2:> by FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Re f) * R2-to-C) ) by A12, FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom u02 ) by A3, FUNCT_1:11;
then  x0 in (dom u02) /\ AB by XBOOLE_0:def_4;
hence  x0 in dom (u02 | AB) by RELAT_1:61; ::_thesis: verum
end;
 for x0 being set st x0 in dom (u02 | AB) holds
x0 in dom (u01 | AB)
proof
let x0 be set ; ::_thesis: ( x0 in dom (u02 | AB) implies x0 in dom (u01 | AB) )
assume A13: x0 in dom (u02 | AB) ; ::_thesis: x0 in dom (u01 | AB)
 x0 in (dom u02) /\ AB by A13, RELAT_1:61;
then A14: ( x0 in dom u02 & x0 in AB ) by XBOOLE_0:def_4;
then  ( x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Re f) * R2-to-C) & x0 in AB ) by A3, FUNCT_1:11;
then  ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_3:def_7;
then  ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then  ( x0 in AB & [((x1 | AB) . x0),((y1 | AB) . x0)] in dom ((Re f) * R2-to-C) ) by A1, FUNCT_1:49;
then  ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then A15: ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
 x0 in (dom x1) /\ (dom y1) by A1, A14, XBOOLE_0:def_4;
then  x0 in dom <:x1,y1:> by FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Re f) * R2-to-C) ) by A15, FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom u01 ) by A2, FUNCT_1:11;
then  x0 in (dom u01) /\ AB by XBOOLE_0:def_4;
hence  x0 in dom (u01 | AB) by RELAT_1:61; ::_thesis: verum
end;
hence  dom (u01 | AB) = dom (u02 | AB) by A9, TARSKI:1; ::_thesis: verum
end;
 for x0 being set st x0 in dom (u01 | AB) holds
(u01 | AB) . x0 = (u02 | AB) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (u01 | AB) implies (u01 | AB) . x0 = (u02 | AB) . x0 )
assume A16: x0 in dom (u01 | AB) ; ::_thesis: (u01 | AB) . x0 = (u02 | AB) . x0
 x0 in (dom u01) /\ AB by A16, RELAT_1:61;
then A17: ( x0 in AB & x0 in dom u01 ) by XBOOLE_0:def_4;
then reconsider x0 = x0 as Real ;
A18: AB c= (dom x1) /\ (dom y1) by A1, XBOOLE_1:19;
then  x0 in (dom x1) /\ (dom y1) by A17;
then  x0 in dom <:x1,y1:> by FUNCT_3:def_7;
then A19: u01 . x0 = ((Re f) * R2-to-C) . (<:x1,y1:> . x0) by A2, FUNCT_1:13;
A20: AB c= (dom x2) /\ (dom y2) by A1, XBOOLE_1:19;
then  x0 in (dom x2) /\ (dom y2) by A17;
then  x0 in dom <:x2,y2:> by FUNCT_3:def_7;
then  u02 . x0 = ((Re f) * R2-to-C) . (<:x2,y2:> . x0) by A3, FUNCT_1:13;
then A21: u02 . x0 = ((Re f) * R2-to-C) . [(x2 . x0),(y2 . x0)] by A17, A20, FUNCT_3:48;
A22: x1 . x0 = (x1 | [.a,b.]) . x0 by A17, FUNCT_1:49
.= x2 . x0 by A17, A1, FUNCT_1:49 ;
A23: y1 . x0 = (y1 | [.a,b.]) . x0 by A17, FUNCT_1:49
.= y2 . x0 by A17, A1, FUNCT_1:49 ;
 ( u01 . x0 = (u01 | AB) . x0 & u02 . x0 = (u02 | AB) . x0 ) by A17, FUNCT_1:49;
hence  (u01 | AB) . x0 = (u02 | AB) . x0 by A17, A18, A19, A21, A22, A23, FUNCT_3:48; ::_thesis: verum
end;
hence  u01 | AB = u02 | AB by A8, FUNCT_1:def_11; ::_thesis: verum
end;
A24: (x1 `| Z) | AB = (x2 `| Z) | AB
proof
A25: dom ((x1 `| Z) | AB) = (dom (x1 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def_7
.= AB by A1, XBOOLE_1:28 ;
A26: dom ((x2 `| Z) | AB) = (dom (x2 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def_7
.= AB by A1, XBOOLE_1:28 ;
 for x0 being set st x0 in dom ((x1 `| Z) | AB) holds
((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom ((x1 `| Z) | AB) implies ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0 )
assume A27: x0 in dom ((x1 `| Z) | AB) ; ::_thesis: ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0
 x0 in dom (x1 `| Z) by A27, RELAT_1:57;
then reconsider x0 = x0 as Real ;
A28: ((x2 `| Z) | AB) . x0 = (x2 `| Z) . x0 by A27, FUNCT_1:49;
A29: (x1 `| Z) . x0 = diff (x1,x0) by A1, A25, A27, FDIFF_1:def_7;
A30: (x2 `| Z) . x0 = diff (x2,x0) by A1, A25, A27, FDIFF_1:def_7;
A31: now__::_thesis:_(_x0_in_].a,b.[_or_x0_=_a_or_x0_=_b_)
assume A32: ( not x0 in ].a,b.[ & not x0 = a & not x0 = b ) ; ::_thesis: contradiction
 x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A25, A27, RCOMP_1:def_1;
then A33: ex r being Real st
( r = x0 & a <= r & r <= b ) ;
A34: now__::_thesis:_(_a_=_x0_or_a_<_x0_)
assume A35: ( not a = x0 & not a < x0 ) ; ::_thesis: contradiction
then  ( 0 < x0 - a or 0 < a - x0 ) by XREAL_1:55;
then  ( a < a + (x0 - a) or 0 < a - x0 ) by XREAL_1:29;
then  ( a < x0 or x0 < x0 + (a - x0) ) by XREAL_1:29;
hence  contradiction by A33, A35; ::_thesis: verum
end;
A36: now__::_thesis:_(_x0_=_b_or_x0_<_b_)
assume A37: ( not x0 = b & not x0 < b ) ; ::_thesis: contradiction
then  ( 0 < x0 - b or 0 < b - x0 ) by XREAL_1:55;
then  ( b < b + (x0 - b) or 0 < b - x0 ) by XREAL_1:29;
then  ( b < x0 or x0 < x0 + (b - x0) ) by XREAL_1:29;
hence  contradiction by A33, A37; ::_thesis: verum
end;
 not x0 in  {  q where q is Real : ( a < q & q < b )  }  by A32, RCOMP_1:def_2;
hence  contradiction by A32, A34, A36; ::_thesis: verum
end;
 diff (x1,x0) = diff (x2,x0)
proof
percases ( x0 = a or x0 in ].a,b.[ or x0 = b ) by A31;
supposeA38: x0 = a ; ::_thesis: diff (x1,x0) = diff (x2,x0)
then  x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A1;
then A39: x0 in [.a,b.] by RCOMP_1:def_1;
then A40: x1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A41: ( x1 is_right_differentiable_in x0 & diff (x1,x0) = Rdiff (x1,x0) ) by FDIFF_3:22;
 x2 is_differentiable_in x0 by A1, A39, FDIFF_1:9;
then A42: ( x2 is_right_differentiable_in x0 & diff (x2,x0) = Rdiff (x2,x0) ) by FDIFF_3:22;
then A43: x1 - x2 is_right_differentiable_in x0 by A41, FDIFF_3:17;
 Rdiff (x1,x0) = Rdiff (x2,x0)
proof
A44: (Rdiff (x1,x0)) - (Rdiff (x2,x0)) = Rdiff ((x1 - x2),x0) by A41, A42, FDIFF_3:17;
 for h being non-zero 0 -convergent Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
let c1 be constant Real_Sequence; ::_thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) implies lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 )
assume A45: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) ) ; ::_thesis: lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A46: ( h is convergent & lim h = 0 ) ;
A47: 0 < b - x0 by A6, A38, XREAL_1:50;
then consider n being Element of NAT  such that
A48: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (b - x0) / 2 by A46, SEQ_2:def_7;
A49: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1
proof
let p1 be real number ; ::_thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1 )
assume A50: 0 < p1 ; ::_thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1
 for m being Element of NAT st n <= m holds
((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 )
assume A51: n <= m ; ::_thesis: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
A52: abs ((h . m) - 0) < (b - x0) / 2 by A48, A51;
A53: 0 < h . m by A45;
then A54: h . m < (b - x0) / 2 by A52, ABSVALUE:def_1;
A55: a + 0 <= x0 + (h . m) by A38, A53, XREAL_1:7;
 x0 + (h . m) <= x0 + ((b - x0) / 2) by A54, XREAL_1:7;
then A56: (x0 + (h . m)) + 0 <= (b - ((b - x0) / 2)) + ((b - x0) / 2) by A47, XREAL_1:7;
A57: [.a,b.] c= (dom x1) /\ (dom x2) by A1, XBOOLE_1:19;
then  x0 in (dom x1) /\ (dom x2) by A39;
then A58: x0 in dom (x1 - x2) by VALUED_1:12;
A59: [.a,b.] c= dom (x1 - x2) by A57, VALUED_1:12;
 x0 + (h . m) in  {  r where r is Real : ( a <= r & r <= b )  }  by A55, A56;
then A60: x0 + (h . m) in [.a,b.] by RCOMP_1:def_1;
A61: x0 in rng c1 by A45, TARSKI:def_1;
A62: lim c1 = c1 . m by SEQ_4:26;
A63: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A61, A62, SEQ_4:25 ;
A64: rng c1 c= dom (x1 - x2)
proof
 for x being set st x in rng c1 holds
x in dom (x1 - x2) by A45, A58, TARSKI:def_1;
hence  rng c1 c= dom (x1 - x2) by TARSKI:def_3; ::_thesis: verum
end;
A65: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = ((h ") . m) * ((((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((x1 - x2) /* (h + c1)) . m) - (((x1 - x2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - (((x1 - x2) /* c1) . m)) by A45, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m))) by A64, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0)) by A61, A62, A63, SEQ_4:25 ;
A66: (x1 - x2) . ((h . m) + x0) = (x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A59, A60, VALUED_1:13
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A60, FUNCT_1:49
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - ((x2 | [.a,b.]) . ((h . m) + x0)) by A60, FUNCT_1:49
.= 0 by A1 ;
(x1 - x2) . x0 = (x1 . x0) - (x2 . x0) by A58, VALUED_1:13
.= ((x1 | [.a,b.]) . x0) - (x2 . x0) by A39, FUNCT_1:49
.= ((x1 | [.a,b.]) . x0) - ((x2 | [.a,b.]) . x0) by A39, FUNCT_1:49
.= 0 by A1 ;
hence  ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A65, A66; ::_thesis: verum
end;
hence  for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1 by A50, COMPLEX1:44; ::_thesis: verum
end;
then  (h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) is convergent by SEQ_2:def_6;
hence  lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 by A49, SEQ_2:def_7; ::_thesis: verum
end;
then  (Rdiff (x1,x0)) - (Rdiff (x2,x0)) = 0 by A43, A44, FDIFF_3:def_6;
hence  Rdiff (x1,x0) = Rdiff (x2,x0) ; ::_thesis: verum
end;
hence  diff (x1,x0) = diff (x2,x0) by A40, A42, FDIFF_3:22; ::_thesis: verum
end;
supposeA67: x0 in ].a,b.[ ; ::_thesis: diff (x1,x0) = diff (x2,x0)
A68: ].a,b.[ is open by RCOMP_1:7;
A69: ].a,b.[ c= [.a,b.]
proof
 for x0 being set st x0 in ].a,b.[ holds
x0 in [.a,b.]
proof
let x0 be set ; ::_thesis: ( x0 in ].a,b.[ implies x0 in [.a,b.] )
assume A70: x0 in ].a,b.[ ; ::_thesis: x0 in [.a,b.]
 x0 in  {  r where r is Real : ( a < r & r < b )  }  by A70, RCOMP_1:def_2;
then A71: ex r being Element of REAL st
( r = x0 & a < r & r < b ) ;
then reconsider x0 = x0 as Real ;
 x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A71;
hence  x0 in [.a,b.] by RCOMP_1:def_1; ::_thesis: verum
end;
hence  ].a,b.[ c= [.a,b.] by TARSKI:def_3; ::_thesis: verum
end;
then A72: x1 is_differentiable_on ].a,b.[ by A1, A68, FDIFF_1:26, XBOOLE_1:1;
then A73: ( x1 | ].a,b.[ is_differentiable_on ].a,b.[ & (x1 | ].a,b.[) `| ].a,b.[ = x1 `| ].a,b.[ ) by A68, FDIFF_2:16;
A74: (x1 `| ].a,b.[) . x0 = diff (x1,x0) by A67, A72, FDIFF_1:def_7;
A75: x2 is_differentiable_on ].a,b.[ by A68, A69, A1, FDIFF_1:26, XBOOLE_1:1;
then A76: ( x2 | ].a,b.[ is_differentiable_on ].a,b.[ & (x2 | ].a,b.[) `| ].a,b.[ = x2 `| ].a,b.[ ) by A68, FDIFF_2:16;
A77: (x2 `| ].a,b.[) . x0 = diff (x2,x0) by A67, A75, FDIFF_1:def_7;
A78: dom (x1 | ].a,b.[) = (dom x1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A69, XBOOLE_1:1, XBOOLE_1:28
.= (dom x2) /\ ].a,b.[ by A1, A69, XBOOLE_1:1, XBOOLE_1:28
.= dom (x2 | ].a,b.[) by RELAT_1:61 ;
 for x0 being set st x0 in dom (x1 | ].a,b.[) holds
(x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (x1 | ].a,b.[) implies (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0 )
assume A79: x0 in dom (x1 | ].a,b.[) ; ::_thesis: (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0
A80: dom (x1 | ].a,b.[) = (dom x1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A69, XBOOLE_1:1, XBOOLE_1:28 ;
then (x1 | ].a,b.[) . x0 = x1 . x0 by A79, FUNCT_1:49
.= (x1 | [.a,b.]) . x0 by A69, A79, A80, FUNCT_1:49
.= x2 . x0 by A69, A79, A80, A1, FUNCT_1:49
.= (x2 | ].a,b.[) . x0 by A79, A80, FUNCT_1:49 ;
hence  (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0 ; ::_thesis: verum
end;
hence  diff (x1,x0) = diff (x2,x0) by A73, A74, A76, A77, A78, FUNCT_1:2; ::_thesis: verum
end;
supposeA81: x0 = b ; ::_thesis: diff (x1,x0) = diff (x2,x0)
then  x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A1;
then A82: x0 in [.a,b.] by RCOMP_1:def_1;
then A83: x1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A84: ( x1 is_left_differentiable_in x0 & diff (x1,x0) = Ldiff (x1,x0) ) by FDIFF_3:22;
 x2 is_differentiable_in x0 by A1, A82, FDIFF_1:9;
then A85: ( x2 is_left_differentiable_in x0 & diff (x2,x0) = Ldiff (x2,x0) ) by FDIFF_3:22;
then A86: x1 - x2 is_left_differentiable_in x0 by A84, FDIFF_3:11;
 Ldiff (x1,x0) = Ldiff (x2,x0)
proof
A87: (Ldiff (x1,x0)) - (Ldiff (x2,x0)) = Ldiff ((x1 - x2),x0) by A84, A85, FDIFF_3:11;
 for h being non-zero 0 -convergent Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
let c1 be constant Real_Sequence; ::_thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) implies lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 )
assume A88: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) ) ; ::_thesis: lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A89: ( h is convergent & lim h = 0 ) ;
A90: 0 < b - a by A6, XREAL_1:50;
then consider n being Element of NAT  such that
A91: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (x0 - a) / 2 by A81, A89, SEQ_2:def_7;
A92: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1
proof
let p1 be real number ; ::_thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1 )
assume A93: 0 < p1 ; ::_thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1
 for m being Element of NAT st n <= m holds
((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 )
assume A94: n <= m ; ::_thesis: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
A95: abs ((h . m) - 0) < (x0 - a) / 2 by A91, A94;
A96: h . m < 0 by A88;
then A97: - (h . m) < (x0 - a) / 2 by A95, ABSVALUE:def_1;
A98: x0 + (h . m) <= b + 0 by A81, A96, XREAL_1:7;
 x0 - ((x0 - a) / 2) <= x0 - (- (h . m)) by A97, XREAL_1:13;
then A99: (a + ((x0 - a) / 2)) - ((x0 - a) / 2) <= (x0 + (h . m)) - 0 by A81, A90, XREAL_1:13;
A100: [.a,b.] c= (dom x1) /\ (dom x2) by A1, XBOOLE_1:19;
then  x0 in (dom x1) /\ (dom x2) by A82;
then A101: x0 in dom (x1 - x2) by VALUED_1:12;
A102: [.a,b.] c= dom (x1 - x2) by A100, VALUED_1:12;
 x0 + (h . m) in  {  r where r is Real : ( a <= r & r <= b )  }  by A98, A99;
then A103: x0 + (h . m) in [.a,b.] by RCOMP_1:def_1;
 x0 in rng c1 by A88, TARSKI:def_1;
then A104: lim c1 = x0 by SEQ_4:25;
A105: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A104, SEQ_4:26 ;
A106: rng c1 c= dom (x1 - x2)
proof
 for x being set st x in rng c1 holds
x in dom (x1 - x2) by A88, A101, TARSKI:def_1;
hence  rng c1 c= dom (x1 - x2) by TARSKI:def_3; ::_thesis: verum
end;
A107: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = ((h ") . m) * ((((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((x1 - x2) /* (h + c1)) . m) - (((x1 - x2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - (((x1 - x2) /* c1) . m)) by A88, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m))) by A106, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0)) by A104, A105, SEQ_4:26 ;
A108: (x1 - x2) . ((h . m) + x0) = (x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A102, A103, VALUED_1:13
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A103, FUNCT_1:49
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - ((x2 | [.a,b.]) . ((h . m) + x0)) by A103, FUNCT_1:49
.= 0 by A1 ;
(x1 - x2) . x0 = (x1 . x0) - (x2 . x0) by A101, VALUED_1:13
.= ((x1 | [.a,b.]) . x0) - (x2 . x0) by A82, FUNCT_1:49
.= ((x1 | [.a,b.]) . x0) - ((x2 | [.a,b.]) . x0) by A82, FUNCT_1:49
.= 0 by A1 ;
hence  ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A107, A108; ::_thesis: verum
end;
hence  for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1 by A93, COMPLEX1:44; ::_thesis: verum
end;
then  (h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) is convergent by SEQ_2:def_6;
hence  lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 by A92, SEQ_2:def_7; ::_thesis: verum
end;
then  Ldiff ((x1 - x2),x0) = 0 by A86, FDIFF_3:def_5;
hence  Ldiff (x1,x0) = Ldiff (x2,x0) by A87; ::_thesis: verum
end;
hence  diff (x1,x0) = diff (x2,x0) by A83, A85, FDIFF_3:22; ::_thesis: verum
end;
end;
end;
hence  ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0 by A27, A28, A29, A30, FUNCT_1:49; ::_thesis: verum
end;
hence  (x1 `| Z) | AB = (x2 `| Z) | AB by A25, A26, FUNCT_1:def_11; ::_thesis: verum
end;
A109: v01 | AB = v02 | AB
proof
A110: dom (v01 | AB) = dom (v02 | AB)
proof
A111: for x0 being set st x0 in dom (v01 | AB) holds
x0 in dom (v02 | AB)
proof
let x0 be set ; ::_thesis: ( x0 in dom (v01 | AB) implies x0 in dom (v02 | AB) )
assume A112: x0 in dom (v01 | AB) ; ::_thesis: x0 in dom (v02 | AB)
 x0 in (dom v01) /\ AB by A112, RELAT_1:61;
then A113: ( x0 in dom v01 & x0 in AB ) by XBOOLE_0:def_4;
then  ( x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Im f) * R2-to-C) & x0 in AB ) by A2, FUNCT_1:11;
then  ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_3:def_7;
then  ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then  ( x0 in AB & [((x2 | AB) . x0),((y2 | AB) . x0)] in dom ((Im f) * R2-to-C) ) by A1, FUNCT_1:49;
then  ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then A114: ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
 x0 in (dom x2) /\ (dom y2) by A1, A113, XBOOLE_0:def_4;
then  x0 in dom <:x2,y2:> by FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Im f) * R2-to-C) ) by A114, FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom v02 ) by A3, FUNCT_1:11;
then  x0 in (dom v02) /\ AB by XBOOLE_0:def_4;
hence  x0 in dom (v02 | AB) by RELAT_1:61; ::_thesis: verum
end;
 for x0 being set st x0 in dom (v02 | AB) holds
x0 in dom (v01 | AB)
proof
let x0 be set ; ::_thesis: ( x0 in dom (v02 | AB) implies x0 in dom (v01 | AB) )
assume A115: x0 in dom (v02 | AB) ; ::_thesis: x0 in dom (v01 | AB)
 x0 in (dom v02) /\ AB by A115, RELAT_1:61;
then A116: ( x0 in dom v02 & x0 in AB ) by XBOOLE_0:def_4;
then  ( x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Im f) * R2-to-C) & x0 in AB ) by A3, FUNCT_1:11;
then  ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_3:def_7;
then  ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then  ( x0 in AB & [((x1 | AB) . x0),((y1 | AB) . x0)] in dom ((Im f) * R2-to-C) ) by A1, FUNCT_1:49;
then  ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then A117: ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
 x0 in (dom x1) /\ (dom y1) by A1, A116, XBOOLE_0:def_4;
then  x0 in dom <:x1,y1:> by FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Im f) * R2-to-C) ) by A117, FUNCT_3:def_7;
then  ( x0 in AB & x0 in dom v01 ) by A2, FUNCT_1:11;
then  x0 in (dom v01) /\ AB by XBOOLE_0:def_4;
hence  x0 in dom (v01 | AB) by RELAT_1:61; ::_thesis: verum
end;
hence  dom (v01 | AB) = dom (v02 | AB) by A111, TARSKI:1; ::_thesis: verum
end;
 for x0 being set st x0 in dom (v01 | AB) holds
(v01 | AB) . x0 = (v02 | AB) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (v01 | AB) implies (v01 | AB) . x0 = (v02 | AB) . x0 )
assume A118: x0 in dom (v01 | AB) ; ::_thesis: (v01 | AB) . x0 = (v02 | AB) . x0
 x0 in (dom v01) /\ AB by A118, RELAT_1:61;
then A119: ( x0 in AB & x0 in dom v01 ) by XBOOLE_0:def_4;
then reconsider x0 = x0 as Real ;
A120: AB c= (dom x1) /\ (dom y1) by A1, XBOOLE_1:19;
then  x0 in (dom x1) /\ (dom y1) by A119;
then  x0 in dom <:x1,y1:> by FUNCT_3:def_7;
then A121: v01 . x0 = ((Im f) * R2-to-C) . (<:x1,y1:> . x0) by A2, FUNCT_1:13;
A122: AB c= (dom x2) /\ (dom y2) by A1, XBOOLE_1:19;
then  x0 in (dom x2) /\ (dom y2) by A119;
then  x0 in dom <:x2,y2:> by FUNCT_3:def_7;
then  v02 . x0 = ((Im f) * R2-to-C) . (<:x2,y2:> . x0) by A3, FUNCT_1:13;
then A123: v02 . x0 = ((Im f) * R2-to-C) . [(x2 . x0),(y2 . x0)] by A119, A122, FUNCT_3:48;
A124: x1 . x0 = (x1 | [.a,b.]) . x0 by A119, FUNCT_1:49
.= x2 . x0 by A119, A1, FUNCT_1:49 ;
A125: y1 . x0 = (y1 | [.a,b.]) . x0 by A119, FUNCT_1:49
.= y2 . x0 by A119, A1, FUNCT_1:49 ;
 ( v01 . x0 = (v01 | AB) . x0 & v02 . x0 = (v02 | AB) . x0 ) by A119, FUNCT_1:49;
hence  (v01 | AB) . x0 = (v02 | AB) . x0 by A124, A125, A121, A119, A120, A123, FUNCT_3:48; ::_thesis: verum
end;
hence  v01 | AB = v02 | AB by A110, FUNCT_1:def_11; ::_thesis: verum
end;
A126: (y1 `| Z) | AB = (y2 `| Z) | AB
proof
A127: dom ((y1 `| Z) | AB) = (dom (y1 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def_7
.= AB by A1, XBOOLE_1:28 ;
A128: dom ((y2 `| Z) | AB) = (dom (y2 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def_7
.= AB by A1, XBOOLE_1:28 ;
 for x0 being set st x0 in dom ((y1 `| Z) | AB) holds
((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom ((y1 `| Z) | AB) implies ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0 )
assume A129: x0 in dom ((y1 `| Z) | AB) ; ::_thesis: ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0
 x0 in dom (y1 `| Z) by A129, RELAT_1:57;
then reconsider x0 = x0 as Real ;
A130: ((y2 `| Z) | AB) . x0 = (y2 `| Z) . x0 by A129, FUNCT_1:49;
A131: (y1 `| Z) . x0 = diff (y1,x0) by A1, A129, A127, FDIFF_1:def_7;
A132: (y2 `| Z) . x0 = diff (y2,x0) by A1, A129, A127, FDIFF_1:def_7;
A133: now__::_thesis:_(_x0_in_].a,b.[_or_x0_=_a_or_x0_=_b_)
assume A134: ( not x0 in ].a,b.[ & not x0 = a & not x0 = b ) ; ::_thesis: contradiction
 x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A127, A129, RCOMP_1:def_1;
then A135: ex r being Real st
( r = x0 & a <= r & r <= b ) ;
A136: now__::_thesis:_(_a_=_x0_or_a_<_x0_)
assume A137: ( not a = x0 & not a < x0 ) ; ::_thesis: contradiction
then  ( 0 < x0 - a or 0 < a - x0 ) by XREAL_1:55;
then  ( a < a + (x0 - a) or 0 < a - x0 ) by XREAL_1:29;
then  ( a < x0 or x0 < x0 + (a - x0) ) by XREAL_1:29;
hence  contradiction by A135, A137; ::_thesis: verum
end;
A138: now__::_thesis:_(_x0_=_b_or_x0_<_b_)
assume A139: ( not x0 = b & not x0 < b ) ; ::_thesis: contradiction
then  ( 0 < x0 - b or 0 < b - x0 ) by XREAL_1:55;
then  ( b < b + (x0 - b) or 0 < b - x0 ) by XREAL_1:29;
then  ( b < x0 or x0 < x0 + (b - x0) ) by XREAL_1:29;
hence  contradiction by A135, A139; ::_thesis: verum
end;
 not x0 in  {  q where q is Real : ( a < q & q < b )  }  by A134, RCOMP_1:def_2;
hence  contradiction by A134, A136, A138; ::_thesis: verum
end;
 diff (y1,x0) = diff (y2,x0)
proof
percases ( x0 = a or x0 in ].a,b.[ or x0 = b ) by A133;
supposeA140: x0 = a ; ::_thesis: diff (y1,x0) = diff (y2,x0)
then  x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A1;
then A141: x0 in [.a,b.] by RCOMP_1:def_1;
then A142: y1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A143: ( y1 is_right_differentiable_in x0 & diff (y1,x0) = Rdiff (y1,x0) ) by FDIFF_3:22;
 y2 is_differentiable_in x0 by A1, A141, FDIFF_1:9;
then A144: ( y2 is_right_differentiable_in x0 & diff (y2,x0) = Rdiff (y2,x0) ) by FDIFF_3:22;
then A145: y1 - y2 is_right_differentiable_in x0 by A143, FDIFF_3:17;
 Rdiff (y1,x0) = Rdiff (y2,x0)
proof
A146: (Rdiff (y1,x0)) - (Rdiff (y2,x0)) = Rdiff ((y1 - y2),x0) by A143, A144, FDIFF_3:17;
 for h being non-zero 0 -convergent Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
let c1 be constant Real_Sequence; ::_thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) implies lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 )
assume A147: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) ) ; ::_thesis: lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A148: ( h is convergent & lim h = 0 ) ;
A149: 0 < b - x0 by A6, A140, XREAL_1:50;
then consider n being Element of NAT  such that
A150: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (b - x0) / 2 by A148, SEQ_2:def_7;
A151: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1
proof
let p1 be real number ; ::_thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1 )
assume A152: 0 < p1 ; ::_thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1
 for m being Element of NAT st n <= m holds
((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 )
assume A153: n <= m ; ::_thesis: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
A154: abs ((h . m) - 0) < (b - x0) / 2 by A150, A153;
A155: 0 < h . m by A147;
then A156: h . m < (b - x0) / 2 by A154, ABSVALUE:def_1;
A157: a + 0 <= x0 + (h . m) by A140, A155, XREAL_1:7;
 x0 + (h . m) <= x0 + ((b - x0) / 2) by A156, XREAL_1:7;
then A158: (x0 + (h . m)) + 0 <= (b - ((b - x0) / 2)) + ((b - x0) / 2) by A149, XREAL_1:7;
A159: [.a,b.] c= (dom y1) /\ (dom y2) by A1, XBOOLE_1:19;
then  x0 in (dom y1) /\ (dom y2) by A141;
then A160: x0 in dom (y1 - y2) by VALUED_1:12;
A161: [.a,b.] c= dom (y1 - y2) by A159, VALUED_1:12;
 x0 + (h . m) in  {  r where r is Real : ( a <= r & r <= b )  }  by A157, A158;
then A162: x0 + (h . m) in [.a,b.] by RCOMP_1:def_1;
A163: x0 in rng c1 by A147, TARSKI:def_1;
A164: lim c1 = c1 . m by SEQ_4:26;
A165: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A164, A163, SEQ_4:25 ;
A166: rng c1 c= dom (y1 - y2)
proof
 for x being set st x in rng c1 holds
x in dom (y1 - y2) by A160, A147, TARSKI:def_1;
hence  rng c1 c= dom (y1 - y2) by TARSKI:def_3; ::_thesis: verum
end;
A167: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = ((h ") . m) * ((((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((y1 - y2) /* (h + c1)) . m) - (((y1 - y2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - (((y1 - y2) /* c1) . m)) by A147, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m))) by A166, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0)) by A163, A164, A165, SEQ_4:25 ;
A168: (y1 - y2) . ((h . m) + x0) = (y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A161, A162, VALUED_1:13
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A162, FUNCT_1:49
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - ((y2 | [.a,b.]) . ((h . m) + x0)) by A162, FUNCT_1:49
.= 0 by A1 ;
(y1 - y2) . x0 = (y1 . x0) - (y2 . x0) by A160, VALUED_1:13
.= ((y1 | [.a,b.]) . x0) - (y2 . x0) by A141, FUNCT_1:49
.= ((y1 | [.a,b.]) . x0) - ((y2 | [.a,b.]) . x0) by A141, FUNCT_1:49
.= 0 by A1 ;
hence  ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A167, A168; ::_thesis: verum
end;
hence  for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1 by A152, COMPLEX1:44; ::_thesis: verum
end;
then  (h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) is convergent by SEQ_2:def_6;
hence  lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 by A151, SEQ_2:def_7; ::_thesis: verum
end;
then  (Rdiff (y1,x0)) - (Rdiff (y2,x0)) = 0 by A145, A146, FDIFF_3:def_6;
hence  Rdiff (y1,x0) = Rdiff (y2,x0) ; ::_thesis: verum
end;
hence  diff (y1,x0) = diff (y2,x0) by A142, A144, FDIFF_3:22; ::_thesis: verum
end;
supposeA169: x0 in ].a,b.[ ; ::_thesis: diff (y1,x0) = diff (y2,x0)
A170: ].a,b.[ is open by RCOMP_1:7;
A171: ].a,b.[ c= [.a,b.]
proof
 for x0 being set st x0 in ].a,b.[ holds
x0 in [.a,b.]
proof
let x0 be set ; ::_thesis: ( x0 in ].a,b.[ implies x0 in [.a,b.] )
assume A172: x0 in ].a,b.[ ; ::_thesis: x0 in [.a,b.]
 x0 in  {  r where r is Real : ( a < r & r < b )  }  by A172, RCOMP_1:def_2;
then A173: ex r being Element of REAL st
( r = x0 & a < r & r < b ) ;
then reconsider x0 = x0 as Real ;
 x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A173;
hence  x0 in [.a,b.] by RCOMP_1:def_1; ::_thesis: verum
end;
hence  ].a,b.[ c= [.a,b.] by TARSKI:def_3; ::_thesis: verum
end;
then A174: y1 is_differentiable_on ].a,b.[ by A1, A170, FDIFF_1:26, XBOOLE_1:1;
then A175: ( y1 | ].a,b.[ is_differentiable_on ].a,b.[ & (y1 | ].a,b.[) `| ].a,b.[ = y1 `| ].a,b.[ ) by A170, FDIFF_2:16;
A176: (y1 `| ].a,b.[) . x0 = diff (y1,x0) by A169, A174, FDIFF_1:def_7;
A177: y2 is_differentiable_on ].a,b.[ by A1, A170, A171, FDIFF_1:26, XBOOLE_1:1;
then A178: ( y2 | ].a,b.[ is_differentiable_on ].a,b.[ & (y2 | ].a,b.[) `| ].a,b.[ = y2 `| ].a,b.[ ) by A170, FDIFF_2:16;
A179: (y2 `| ].a,b.[) . x0 = diff (y2,x0) by A169, A177, FDIFF_1:def_7;
A180: dom (y1 | ].a,b.[) = (dom y1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A171, XBOOLE_1:1, XBOOLE_1:28
.= (dom y2) /\ ].a,b.[ by A1, A171, XBOOLE_1:1, XBOOLE_1:28
.= dom (y2 | ].a,b.[) by RELAT_1:61 ;
 for x0 being set st x0 in dom (y1 | ].a,b.[) holds
(y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (y1 | ].a,b.[) implies (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0 )
assume A181: x0 in dom (y1 | ].a,b.[) ; ::_thesis: (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0
A182: dom (y1 | ].a,b.[) = (dom y1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A171, XBOOLE_1:1, XBOOLE_1:28 ;
then (y1 | ].a,b.[) . x0 = y1 . x0 by A181, FUNCT_1:49
.= (y1 | [.a,b.]) . x0 by A171, A181, A182, FUNCT_1:49
.= y2 . x0 by A171, A181, A182, A1, FUNCT_1:49
.= (y2 | ].a,b.[) . x0 by A181, A182, FUNCT_1:49 ;
hence  (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0 ; ::_thesis: verum
end;
hence  diff (y1,x0) = diff (y2,x0) by A175, A176, A178, A179, A180, FUNCT_1:2; ::_thesis: verum
end;
supposeA183: x0 = b ; ::_thesis: diff (y1,x0) = diff (y2,x0)
then  x0 in  {  r where r is Real : ( a <= r & r <= b )  }  by A1;
then A184: x0 in [.a,b.] by RCOMP_1:def_1;
then A185: y1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A186: ( y1 is_left_differentiable_in x0 & diff (y1,x0) = Ldiff (y1,x0) ) by FDIFF_3:22;
 y2 is_differentiable_in x0 by A1, A184, FDIFF_1:9;
then A187: ( y2 is_left_differentiable_in x0 & diff (y2,x0) = Ldiff (y2,x0) ) by FDIFF_3:22;
then A188: y1 - y2 is_left_differentiable_in x0 by A186, FDIFF_3:11;
 Ldiff (y1,x0) = Ldiff (y2,x0)
proof
A189: (Ldiff (y1,x0)) - (Ldiff (y2,x0)) = Ldiff ((y1 - y2),x0) by A186, A187, FDIFF_3:11;
 for h being non-zero 0 -convergent Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
let c1 be constant Real_Sequence; ::_thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) implies lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 )
assume A190: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) ) ; ::_thesis: lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A191: ( h is convergent & lim h = 0 ) ;
A192: 0 < b - a by A6, XREAL_1:50;
then consider n being Element of NAT  such that
A193: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (x0 - a) / 2 by A183, A191, SEQ_2:def_7;
A194: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1
proof
let p1 be real number ; ::_thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1 )
assume A195: 0 < p1 ; ::_thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1
 for m being Element of NAT st n <= m holds
((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 )
assume A196: n <= m ; ::_thesis: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
A197: abs ((h . m) - 0) < (x0 - a) / 2 by A193, A196;
A198: h . m < 0 by A190;
then A199: - (h . m) < (x0 - a) / 2 by A197, ABSVALUE:def_1;
A200: x0 + (h . m) <= b + 0 by A183, A198, XREAL_1:7;
 x0 - ((x0 - a) / 2) <= x0 - (- (h . m)) by A199, XREAL_1:13;
then A201: (a + ((x0 - a) / 2)) - ((x0 - a) / 2) <= (x0 + (h . m)) - 0 by A183, A192, XREAL_1:13;
A202: [.a,b.] c= (dom y1) /\ (dom y2) by A1, XBOOLE_1:19;
then  x0 in (dom y1) /\ (dom y2) by A184;
then A203: x0 in dom (y1 - y2) by VALUED_1:12;
A204: [.a,b.] c= dom (y1 - y2) by A202, VALUED_1:12;
 x0 + (h . m) in  {  r where r is Real : ( a <= r & r <= b )  }  by A200, A201;
then A205: x0 + (h . m) in [.a,b.] by RCOMP_1:def_1;
 x0 in rng c1 by A190, TARSKI:def_1;
then A206: lim c1 = x0 by SEQ_4:25;
A207: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A206, SEQ_4:26 ;
A208: rng c1 c= dom (y1 - y2)
proof
 for x being set st x in rng c1 holds
x in dom (y1 - y2) by A190, A203, TARSKI:def_1;
hence  rng c1 c= dom (y1 - y2) by TARSKI:def_3; ::_thesis: verum
end;
A209: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = ((h ") . m) * ((((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((y1 - y2) /* (h + c1)) . m) - (((y1 - y2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - (((y1 - y2) /* c1) . m)) by A190, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m))) by A208, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0)) by A206, A207, SEQ_4:26 ;
A210: (y1 - y2) . ((h . m) + x0) = (y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A204, A205, VALUED_1:13
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A205, FUNCT_1:49
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - ((y2 | [.a,b.]) . ((h . m) + x0)) by A205, FUNCT_1:49
.= 0 by A1 ;
(y1 - y2) . x0 = (y1 . x0) - (y2 . x0) by A203, VALUED_1:13
.= ((y1 | [.a,b.]) . x0) - (y2 . x0) by A184, FUNCT_1:49
.= ((y1 | [.a,b.]) . x0) - ((y2 | [.a,b.]) . x0) by A184, FUNCT_1:49
.= 0 by A1 ;
hence  ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A209, A210; ::_thesis: verum
end;
hence  for m being Element of NAT st n <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1 by A195, COMPLEX1:44; ::_thesis: verum
end;
then  (h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) is convergent by SEQ_2:def_6;
hence  lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 by A194, SEQ_2:def_7; ::_thesis: verum
end;
then  Ldiff ((y1 - y2),x0) = 0 by A188, FDIFF_3:def_5;
hence  Ldiff (y1,x0) = Ldiff (y2,x0) by A189; ::_thesis: verum
end;
hence  diff (y1,x0) = diff (y2,x0) by A185, A187, FDIFF_3:22; ::_thesis: verum
end;
end;
end;
hence  ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0 by A129, A130, A131, A132, FUNCT_1:49; ::_thesis: verum
end;
hence  (y1 `| Z) | AB = (y2 `| Z) | AB by A127, A128, FUNCT_1:def_11; ::_thesis: verum
end;
A211: ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB
proof
A212: ( x1 `| Z is PartFunc of REAL,COMPLEX & y1 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A213: ( u01 is PartFunc of REAL,COMPLEX & v01 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
 ( u01 (#) (x1 `| Z) is PartFunc of REAL,COMPLEX & v01 (#) (y1 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then A214: ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u01 (#) (x1 `| Z)) | AB) - ((v01 (#) (y1 `| Z)) | AB) by CFUNCT_1:55
.= ((u01 | AB) (#) ((x1 `| Z) | AB)) - ((v01 (#) (y1 `| Z)) | AB) by A212, A213, CFUNCT_1:53
.= ((u01 | AB) (#) ((x1 `| Z) | AB)) - ((v01 | AB) (#) ((y1 `| Z) | AB)) by A212, A213, CFUNCT_1:53 ;
A215: ( x2 `| Z is PartFunc of REAL,COMPLEX & y2 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A216: ( u02 is PartFunc of REAL,COMPLEX & v02 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
 ( u02 (#) (x2 `| Z) is PartFunc of REAL,COMPLEX & v02 (#) (y2 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB = ((u02 (#) (x2 `| Z)) | AB) - ((v02 (#) (y2 `| Z)) | AB) by CFUNCT_1:55
.= ((u02 | AB) (#) ((x2 `| Z) | AB)) - ((v02 (#) (y2 `| Z)) | AB) by A215, A216, CFUNCT_1:53
.= ((u02 | AB) (#) ((x2 `| Z) | AB)) - ((v02 | AB) (#) ((y2 `| Z) | AB)) by A215, A216, CFUNCT_1:53 ;
hence  ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB by A7, A24, A109, A126, A214; ::_thesis: verum
end;
A217: integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b) = integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),AB) by INTEGRA5:19
.= integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),AB) by A211
.= integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) by INTEGRA5:19 ;
A218: ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB
proof
A219: ( x1 `| Z is PartFunc of REAL,COMPLEX & y1 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A220: ( v01 is PartFunc of REAL,COMPLEX & u01 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
 ( v01 (#) (x1 `| Z) is PartFunc of REAL,COMPLEX & u01 (#) (y1 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then A221: ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v01 (#) (x1 `| Z)) | AB) + ((u01 (#) (y1 `| Z)) | AB) by CFUNCT_1:52
.= ((v01 | AB) (#) ((x1 `| Z) | AB)) + ((u01 (#) (y1 `| Z)) | AB) by A219, A220, CFUNCT_1:53
.= ((v01 | AB) (#) ((x1 `| Z) | AB)) + ((u01 | AB) (#) ((y1 `| Z) | AB)) by A219, A220, CFUNCT_1:53 ;
A222: ( x2 `| Z is PartFunc of REAL,COMPLEX & y2 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A223: ( v02 is PartFunc of REAL,COMPLEX & u02 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
 ( v02 (#) (x2 `| Z) is PartFunc of REAL,COMPLEX & u02 (#) (y2 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB = ((v02 (#) (x2 `| Z)) | AB) + ((u02 (#) (y2 `| Z)) | AB) by CFUNCT_1:52
.= ((v02 | AB) (#) ((x2 `| Z) | AB)) + ((u02 (#) (y2 `| Z)) | AB) by A222, A223, CFUNCT_1:53
.= ((v02 | AB) (#) ((x2 `| Z) | AB)) + ((u02 | AB) (#) ((y2 `| Z) | AB)) by A222, A223, CFUNCT_1:53 ;
hence  ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB by A7, A24, A109, A126, A221; ::_thesis: verum
end;
integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b) = integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),AB) by INTEGRA5:19
.= integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),AB) by A218
.= integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b) by INTEGRA5:19 ;
hence  integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z) by A2, A3, A217; ::_thesis: verum
end;
supposeA224: a = b ; ::_thesis: integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)
then reconsider BA = [.b,a.] as non empty closed_interval Subset of REAL by MEASURE5:14;
A225: integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b) = integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),BA) by A224, INTEGRA5:19;
A226: - (integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),BA)) = integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b) by INTEGRA5:20;
A227: integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b) = integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),BA) by A224, INTEGRA5:19;
A228: - (integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),BA)) = integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b) by INTEGRA5:20;
 integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) = integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),BA) by A224, INTEGRA5:19;
then A229: integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) = - (integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b)) by INTEGRA5:20;
 integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b) = integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),AB) by INTEGRA5:19;
then  integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b) = - (integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b)) by A224, INTEGRA5:20;
hence  integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z) by A2, A3, A225, A226, A227, A228, A229; ::_thesis: verum
end;
end;
end;

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
assume A1: rng C c= dom f ;
func integral (f,C) ->  Complex means :Def4: :: INTEGR1C:def 4
 ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & it = integral (f,x,y,a,b,Z) );
existence
 ex b1 being Complex ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b1 = integral (f,x,y,a,b,Z) )
proof
consider a, b being Real, x, y being PartFunc of REAL,REAL, Z being Subset of REAL such that
A2: ( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] ) by Def3;
take  integral (f,x,y,a,b,Z) ; ::_thesis: ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & integral (f,x,y,a,b,Z) = integral (f,x,y,a,b,Z) )
thus  ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & integral (f,x,y,a,b,Z) = integral (f,x,y,a,b,Z) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Complex st ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b1 = integral (f,x,y,a,b,Z) ) & ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b2 = integral (f,x,y,a,b,Z) ) holds
b1 = b2
proof
let s1, s2 be Complex; ::_thesis: ( ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & s1 = integral (f,x,y,a,b,Z) ) & ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & s2 = integral (f,x,y,a,b,Z) ) implies s1 = s2 )
assume A3: ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & s1 = integral (f,x,y,a,b,Z) ) ; ::_thesis: ( for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL holds
( not a <= b or not [.a,b.] = dom C or not [.a,b.] c= dom x or not [.a,b.] c= dom y or not Z is open or not [.a,b.] c= Z or not x is_differentiable_on Z or not y is_differentiable_on Z or not x `| Z is continuous or not y `| Z is continuous or not C = (x + (<i> (#) y)) | [.a,b.] or not s2 = integral (f,x,y,a,b,Z) ) or s1 = s2 )
assume A4: ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & s2 = integral (f,x,y,a,b,Z) ) ; ::_thesis: s1 = s2
consider a1, b1 being Real, x1, y1 being PartFunc of REAL,REAL, Z1 being Subset of REAL such that
A5: ( a1 <= b1 & [.a1,b1.] = dom C & [.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 & C = (x1 + (<i> (#) y1)) | [.a1,b1.] & s1 = integral (f,x1,y1,a1,b1,Z1) ) by A3;
consider a2, b2 being Real, x2, y2 being PartFunc of REAL,REAL, Z2 being Subset of REAL such that
A6: ( a2 <= b2 & [.a2,b2.] = dom C & [.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 & C = (x2 + (<i> (#) y2)) | [.a2,b2.] & s2 = integral (f,x2,y2,a2,b2,Z2) ) by A4;
 dom C is non empty closed_interval Subset of REAL by A5, MEASURE5:14;
then A7: ( a1 = a2 & b1 = b2 ) by A6, A5, INTEGRA1:5;
reconsider Z3 = Z1 /\ Z2 as Subset of REAL ;
reconsider ZZ1 = Z1, ZZ2 = Z2 as Subset of R^1 by TOPMETR:17;
 ( ZZ1 is open & ZZ2 is open ) by A5, A6, BORSUK_5:39;
then  ZZ1 /\ ZZ2 is open by TOPS_1:11;
then A8: Z3 is open by BORSUK_5:39;
A9: x1 | [.a1,b1.] = x2 | [.a2,b2.]
proof
 for x0 being set st x0 in [.a1,b1.] holds
x1 . x0 = x2 . x0
proof
let x0 be set ; ::_thesis: ( x0 in [.a1,b1.] implies x1 . x0 = x2 . x0 )
assume A10: x0 in [.a1,b1.] ; ::_thesis: x1 . x0 = x2 . x0
A11: dom (<i> (#) y1) = dom y1 by VALUED_1:def_5;
 dom (x1 + (<i> (#) y1)) = (dom x1) /\ (dom (<i> (#) y1)) by VALUED_1:def_1;
then A12: [.a1,b1.] c= dom (x1 + (<i> (#) y1)) by A5, A11, XBOOLE_1:19;
A13: ((x1 + (<i> (#) y1)) | [.a1,b1.]) . x0 = (x1 + (<i> (#) y1)) . x0 by A10, FUNCT_1:49
.= (x1 . x0) + ((<i> (#) y1) . x0) by A10, A12, VALUED_1:def_1
.= (x1 . x0) + (<i> * (y1 . x0)) by VALUED_1:6 ;
A14: dom (<i> (#) y2) = dom y2 by VALUED_1:def_5;
 dom (x2 + (<i> (#) y2)) = (dom x2) /\ (dom (<i> (#) y2)) by VALUED_1:def_1;
then A15: [.a2,b2.] c= dom (x2 + (<i> (#) y2)) by A6, A14, XBOOLE_1:19;
((x2 + (<i> (#) y2)) | [.a2,b2.]) . x0 = (x2 + (<i> (#) y2)) . x0 by A6, A5, A10, FUNCT_1:49
.= (x2 . x0) + ((<i> (#) y2) . x0) by A6, A5, A10, A15, VALUED_1:def_1
.= (x2 . x0) + (<i> * (y2 . x0)) by VALUED_1:6 ;
hence  x1 . x0 = x2 . x0 by A6, A5, A13, COMPLEX1:77; ::_thesis: verum
end;
hence  x1 | [.a1,b1.] = x2 | [.a2,b2.] by A5, A6, FUNCT_1:95; ::_thesis: verum
end;
A16: y1 | [.a1,b1.] = y2 | [.a2,b2.]
proof
 for x0 being set st x0 in [.a1,b1.] holds
y1 . x0 = y2 . x0
proof
let x0 be set ; ::_thesis: ( x0 in [.a1,b1.] implies y1 . x0 = y2 . x0 )
assume A17: x0 in [.a1,b1.] ; ::_thesis: y1 . x0 = y2 . x0
A18: dom (<i> (#) y1) = dom y1 by VALUED_1:def_5;
 dom (x1 + (<i> (#) y1)) = (dom x1) /\ (dom (<i> (#) y1)) by VALUED_1:def_1;
then A19: [.a1,b1.] c= dom (x1 + (<i> (#) y1)) by A5, A18, XBOOLE_1:19;
A20: ((x1 + (<i> (#) y1)) | [.a1,b1.]) . x0 = (x1 + (<i> (#) y1)) . x0 by A17, FUNCT_1:49
.= (x1 . x0) + ((<i> (#) y1) . x0) by A17, A19, VALUED_1:def_1
.= (x1 . x0) + (<i> * (y1 . x0)) by VALUED_1:6 ;
A21: dom (<i> (#) y2) = dom y2 by VALUED_1:def_5;
 dom (x2 + (<i> (#) y2)) = (dom x2) /\ (dom (<i> (#) y2)) by VALUED_1:def_1;
then A22: [.a2,b2.] c= dom (x2 + (<i> (#) y2)) by A6, A21, XBOOLE_1:19;
((x2 + (<i> (#) y2)) | [.a2,b2.]) . x0 = (x2 + (<i> (#) y2)) . x0 by A5, A6, A17, FUNCT_1:49
.= (x2 . x0) + ((<i> (#) y2) . x0) by A5, A6, A17, A22, VALUED_1:def_1
.= (x2 . x0) + (<i> * (y2 . x0)) by VALUED_1:6 ;
hence  y1 . x0 = y2 . x0 by A6, A5, A20, COMPLEX1:77; ::_thesis: verum
end;
hence  y1 | [.a1,b1.] = y2 | [.a2,b2.] by A5, A6, FUNCT_1:95; ::_thesis: verum
end;
A23: [.a1,b1.] c= Z3 by A5, A6, XBOOLE_1:19;
A24: ( x1 is_differentiable_on Z3 & y1 is_differentiable_on Z3 ) by A5, A8, FDIFF_1:26, XBOOLE_1:17;
A25: ( x2 is_differentiable_on Z3 & y2 is_differentiable_on Z3 ) by A6, A8, FDIFF_1:26, XBOOLE_1:17;
thus s1 = integral (f,x1,y1,a1,b1,Z3) by A1, A5, A8, A23, Lm1, XBOOLE_1:17
.= integral (f,x2,y2,a2,b2,Z3) by A1, A5, A6, A7, A8, A9, A16, A24, A25, Lm2, XBOOLE_1:19
.= s2 by A1, A6, A5, A8, A23, Lm1, XBOOLE_1:17 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines integral INTEGR1C:def_4_:_
 for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f holds
for b3 being Complex holds
( b3 = integral (f,C) iff ex a, b being Real ex x, y being PartFunc of REAL,REAL ex Z being Subset of REAL st
( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] & b3 = integral (f,x,y,a,b,Z) ) );

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
predf is_integrable_on C means :Def5: :: INTEGR1C:def 5
 for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( (u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is_integrable_on ['a,b'] & (v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is_integrable_on ['a,b'] );
end;

:: deftheorem Def5 defines is_integrable_on INTEGR1C:def_5_:_
 for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve holds
( f is_integrable_on C iff for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( (u0 (#) (x `| Z)) - (v0 (#) (y `| Z)) is_integrable_on ['a,b'] & (v0 (#) (x `| Z)) + (u0 (#) (y `| Z)) is_integrable_on ['a,b'] ) );

definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
predf is_bounded_on C means :Def6: :: INTEGR1C:def 6
 for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded & ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded );
end;

:: deftheorem Def6 defines is_bounded_on INTEGR1C:def_6_:_
 for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve holds
( f is_bounded_on C iff for a, b being Real
for x, y being PartFunc of REAL,REAL
for Z being Subset of REAL
for u0, v0 being PartFunc of REAL,REAL st a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] holds
( ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) | ['a,b'] is bounded & ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) | ['a,b'] is bounded ) );

begin

theorem :: INTEGR1C:1
for f, g being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f & rng C c= dom g & f is_integrable_on C & g is_integrable_on C & f is_bounded_on C & g is_bounded_on C holds
integral ((f + g),C) = (integral (f,C)) + (integral (g,C))
proof
let f, g be PartFunc of COMPLEX,COMPLEX; ::_thesis: for C being C1-curve st rng C c= dom f & rng C c= dom g & f is_integrable_on C & g is_integrable_on C & f is_bounded_on C & g is_bounded_on C holds
integral ((f + g),C) = (integral (f,C)) + (integral (g,C))
let C be C1-curve; ::_thesis: ( rng C c= dom f & rng C c= dom g & f is_integrable_on C & g is_integrable_on C & f is_bounded_on C & g is_bounded_on C implies integral ((f + g),C) = (integral (f,C)) + (integral (g,C)) )
assume A1: ( rng C c= dom f & rng C c= dom g & f is_integrable_on C & g is_integrable_on C & f is_bounded_on C & g is_bounded_on C ) ; ::_thesis: integral ((f + g),C) = (integral (f,C)) + (integral (g,C))
consider a, b being Real, x, y being PartFunc of REAL,REAL, Z being Subset of REAL such that
A2: ( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] ) by Def3;
consider uf0, vf0 being PartFunc of REAL,REAL such that
A3: ( uf0 = ((Re f) * R2-to-C) * <:x,y:> & vf0 = ((Im f) * R2-to-C) * <:x,y:> & integral (f,x,y,a,b,Z) = (integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + ((integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b)) * <i>) ) by Def2;
consider ug0, vg0 being PartFunc of REAL,REAL such that
A4: ( ug0 = ((Re g) * R2-to-C) * <:x,y:> & vg0 = ((Im g) * R2-to-C) * <:x,y:> & integral (g,x,y,a,b,Z) = (integral (((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))),a,b)) + ((integral (((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z))),a,b)) * <i>) ) by Def2;
A5: ( integral (f,C) = integral (f,x,y,a,b,Z) & integral (g,C) = integral (g,x,y,a,b,Z) ) by A1, A2, Def4;
A6: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
A7: rng C c= (dom f) /\ (dom g) by A1, XBOOLE_1:19;
consider u0, v0 being PartFunc of REAL,REAL such that
A8: ( u0 = ((Re (f + g)) * R2-to-C) * <:x,y:> & v0 = ((Im (f + g)) * R2-to-C) * <:x,y:> & integral ((f + g),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;
A9: u0 (#) (x `| Z) = (uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))
proof
A10: dom ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) = (dom (uf0 (#) (x `| Z))) /\ (dom (ug0 (#) (x `| Z))) by VALUED_1:def_1
.= ((dom uf0) /\ (dom (x `| Z))) /\ (dom (ug0 (#) (x `| Z))) by VALUED_1:def_4
.= ((dom uf0) /\ (dom (x `| Z))) /\ ((dom ug0) /\ (dom (x `| Z))) by VALUED_1:def_4
.= (dom uf0) /\ ((dom (x `| Z)) /\ ((dom ug0) /\ (dom (x `| Z)))) by XBOOLE_1:16
.= (dom uf0) /\ (((dom (x `| Z)) /\ (dom (x `| Z))) /\ (dom ug0)) by XBOOLE_1:16
.= ((dom uf0) /\ (dom ug0)) /\ (dom (x `| Z)) by XBOOLE_1:16 ;
A11: dom (u0 (#) (x `| Z)) = (dom u0) /\ (dom (x `| Z)) by VALUED_1:def_4;
A12: dom u0 = (dom uf0) /\ (dom ug0)
proof
A13: for x0 being set st x0 in dom u0 holds
x0 in (dom uf0) /\ (dom ug0)
proof
let x0 be set ; ::_thesis: ( x0 in dom u0 implies x0 in (dom uf0) /\ (dom ug0) )
assume A14: x0 in dom u0 ; ::_thesis: x0 in (dom uf0) /\ (dom ug0)
A15: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C) ) by A14, A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A16: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) ) by A15, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g)) by MESFUN6C:5;
then  R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g)) by VALUED_1:def_1;
then  ( R2-to-C . (<:x,y:> . x0) in dom (Re f) & R2-to-C . (<:x,y:> . x0) in dom (Re g) ) by XBOOLE_0:def_4;
then  ( <:x,y:> . x0 in dom ((Re f) * R2-to-C) & <:x,y:> . x0 in dom ((Re g) * R2-to-C) ) by A16, FUNCT_1:11;
then  ( x0 in dom uf0 & x0 in dom ug0 ) by A3, A4, A15, FUNCT_1:11;
hence  x0 in (dom uf0) /\ (dom ug0) by XBOOLE_0:def_4; ::_thesis: verum
end;
 for x0 being set st x0 in (dom uf0) /\ (dom ug0) holds
x0 in dom u0
proof
let x0 be set ; ::_thesis: ( x0 in (dom uf0) /\ (dom ug0) implies x0 in dom u0 )
assume A17: x0 in (dom uf0) /\ (dom ug0) ; ::_thesis: x0 in dom u0
A18: ( x0 in dom uf0 & x0 in dom ug0 ) by A17, XBOOLE_0:def_4;
then A19: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A20: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re g) * R2-to-C) ) by A18, A4, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A21: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re f) ) by A19, FUNCT_1:11;
 ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re g) ) by A20, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g)) by A21, XBOOLE_0:def_4;
then  R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g)) by VALUED_1:def_1;
then  R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) by MESFUN6C:5;
then  <:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C) by A21, FUNCT_1:11;
hence  x0 in dom u0 by A8, A19, FUNCT_1:11; ::_thesis: verum
end;
hence  dom u0 = (dom uf0) /\ (dom ug0) by A13, TARSKI:1; ::_thesis: verum
end;
 for x0 being set st x0 in dom (u0 (#) (x `| Z)) holds
(u0 (#) (x `| Z)) . x0 = ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (u0 (#) (x `| Z)) implies (u0 (#) (x `| Z)) . x0 = ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0 )
assume A22: x0 in dom (u0 (#) (x `| Z)) ; ::_thesis: (u0 (#) (x `| Z)) . x0 = ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0
 x0 in (dom u0) /\ (dom (x `| Z)) by A22, VALUED_1:def_4;
then A23: ( x0 in dom u0 & x0 in dom (x `| Z) ) by XBOOLE_0:def_4;
then A24: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C) ) by A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A25: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) ) by A24, FUNCT_1:11;
set c0 = R2-to-C . (<:x,y:> . x0);
A26: u0 . x0 = ((Re (f + g)) * R2-to-C) . (<:x,y:> . x0) by A8, A23, FUNCT_1:12
.= (Re (f + g)) . (R2-to-C . (<:x,y:> . x0)) by A24, FUNCT_1:12
.= ((Re f) + (Re g)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:5 ;
A27: R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g)) by A25, MESFUN6C:5;
A28: ( x0 in dom uf0 & x0 in dom ug0 ) by A12, A23, XBOOLE_0:def_4;
then A29: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A30: uf0 . x0 = ((Re f) * R2-to-C) . (<:x,y:> . x0) by A3, A28, FUNCT_1:12
.= (Re f) . (R2-to-C . (<:x,y:> . x0)) by A29, FUNCT_1:12 ;
A31: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re g) * R2-to-C) ) by A4, A28, FUNCT_1:11;
A32: ug0 . x0 = ((Re g) * R2-to-C) . (<:x,y:> . x0) by A4, A28, FUNCT_1:12
.= (Re g) . (R2-to-C . (<:x,y:> . x0)) by A31, FUNCT_1:12 ;
 x0 in (dom (uf0 (#) (x `| Z))) /\ (dom (ug0 (#) (x `| Z))) by A10, A11, A12, A22, VALUED_1:def_1;
then A33: ( x0 in dom (uf0 (#) (x `| Z)) & x0 in dom (ug0 (#) (x `| Z)) ) by XBOOLE_0:def_4;
then A34: (uf0 (#) (x `| Z)) . x0 = ((Re f) . (R2-to-C . (<:x,y:> . x0))) * ((x `| Z) . x0) by A30, VALUED_1:def_4;
A35: (ug0 (#) (x `| Z)) . x0 = ((Re g) . (R2-to-C . (<:x,y:> . x0))) * ((x `| Z) . x0) by A32, A33, VALUED_1:def_4;
(u0 (#) (x `| Z)) . x0 = (u0 . x0) * ((x `| Z) . x0) by A22, VALUED_1:def_4
.= (((Re f) . (R2-to-C . (<:x,y:> . x0))) + ((Re g) . (R2-to-C . (<:x,y:> . x0)))) * ((x `| Z) . x0) by A26, A27, VALUED_1:def_1
.= ((uf0 (#) (x `| Z)) . x0) + ((ug0 (#) (x `| Z)) . x0) by A35, A34
.= ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0 by A10, A11, A12, A22, VALUED_1:def_1 ;
hence  (u0 (#) (x `| Z)) . x0 = ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0 ; ::_thesis: verum
end;
hence  u0 (#) (x `| Z) = (uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z)) by A10, A11, A12, FUNCT_1:2; ::_thesis: verum
end;
A36: v0 (#) (x `| Z) = (vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))
proof
A37: dom ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) = (dom (vf0 (#) (x `| Z))) /\ (dom (vg0 (#) (x `| Z))) by VALUED_1:def_1
.= ((dom vf0) /\ (dom (x `| Z))) /\ (dom (vg0 (#) (x `| Z))) by VALUED_1:def_4
.= ((dom vf0) /\ (dom (x `| Z))) /\ ((dom vg0) /\ (dom (x `| Z))) by VALUED_1:def_4
.= (dom vf0) /\ ((dom (x `| Z)) /\ ((dom vg0) /\ (dom (x `| Z)))) by XBOOLE_1:16
.= (dom vf0) /\ (((dom (x `| Z)) /\ (dom (x `| Z))) /\ (dom vg0)) by XBOOLE_1:16
.= ((dom vf0) /\ (dom vg0)) /\ (dom (x `| Z)) by XBOOLE_1:16 ;
A38: dom (v0 (#) (x `| Z)) = (dom v0) /\ (dom (x `| Z)) by VALUED_1:def_4;
A39: dom v0 = (dom vf0) /\ (dom vg0)
proof
A40: for x0 being set st x0 in dom v0 holds
x0 in (dom vf0) /\ (dom vg0)
proof
let x0 be set ; ::_thesis: ( x0 in dom v0 implies x0 in (dom vf0) /\ (dom vg0) )
assume A41: x0 in dom v0 ; ::_thesis: x0 in (dom vf0) /\ (dom vg0)
A42: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C) ) by A41, A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A43: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) ) by A42, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g)) by MESFUN6C:5;
then  R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g)) by VALUED_1:def_1;
then  ( R2-to-C . (<:x,y:> . x0) in dom (Im f) & R2-to-C . (<:x,y:> . x0) in dom (Im g) ) by XBOOLE_0:def_4;
then  ( <:x,y:> . x0 in dom ((Im f) * R2-to-C) & <:x,y:> . x0 in dom ((Im g) * R2-to-C) ) by A43, FUNCT_1:11;
then  ( x0 in dom vf0 & x0 in dom vg0 ) by A3, A4, A42, FUNCT_1:11;
hence  x0 in (dom vf0) /\ (dom vg0) by XBOOLE_0:def_4; ::_thesis: verum
end;
 for x0 being set st x0 in (dom vf0) /\ (dom vg0) holds
x0 in dom v0
proof
let x0 be set ; ::_thesis: ( x0 in (dom vf0) /\ (dom vg0) implies x0 in dom v0 )
assume A44: x0 in (dom vf0) /\ (dom vg0) ; ::_thesis: x0 in dom v0
A45: ( x0 in dom vf0 & x0 in dom vg0 ) by A44, XBOOLE_0:def_4;
then A46: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A47: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im g) * R2-to-C) ) by A45, A4, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A48: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im f) ) by A46, FUNCT_1:11;
 ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im g) ) by A47, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g)) by A48, XBOOLE_0:def_4;
then  R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g)) by VALUED_1:def_1;
then  R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) by MESFUN6C:5;
then  <:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C) by A48, FUNCT_1:11;
hence  x0 in dom v0 by A8, A46, FUNCT_1:11; ::_thesis: verum
end;
hence  dom v0 = (dom vf0) /\ (dom vg0) by A40, TARSKI:1; ::_thesis: verum
end;
 for x0 being set st x0 in dom (v0 (#) (x `| Z)) holds
(v0 (#) (x `| Z)) . x0 = ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (v0 (#) (x `| Z)) implies (v0 (#) (x `| Z)) . x0 = ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0 )
assume A49: x0 in dom (v0 (#) (x `| Z)) ; ::_thesis: (v0 (#) (x `| Z)) . x0 = ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0
 x0 in (dom v0) /\ (dom (x `| Z)) by A49, VALUED_1:def_4;
then A50: ( x0 in dom v0 & x0 in dom (x `| Z) ) by XBOOLE_0:def_4;
then A51: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C) ) by A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A52: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) ) by A51, FUNCT_1:11;
set c0 = R2-to-C . (<:x,y:> . x0);
A53: v0 . x0 = ((Im (f + g)) * R2-to-C) . (<:x,y:> . x0) by A8, A50, FUNCT_1:12
.= (Im (f + g)) . (R2-to-C . (<:x,y:> . x0)) by A51, FUNCT_1:12
.= ((Im f) + (Im g)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:5 ;
A54: R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g)) by A52, MESFUN6C:5;
A55: ( x0 in dom vf0 & x0 in dom vg0 ) by A39, A50, XBOOLE_0:def_4;
then A56: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A57: vf0 . x0 = ((Im f) * R2-to-C) . (<:x,y:> . x0) by A3, A55, FUNCT_1:12
.= (Im f) . (R2-to-C . (<:x,y:> . x0)) by A56, FUNCT_1:12 ;
A58: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im g) * R2-to-C) ) by A4, A55, FUNCT_1:11;
A59: vg0 . x0 = ((Im g) * R2-to-C) . (<:x,y:> . x0) by A4, A55, FUNCT_1:12
.= (Im g) . (R2-to-C . (<:x,y:> . x0)) by A58, FUNCT_1:12 ;
 x0 in (dom (vf0 (#) (x `| Z))) /\ (dom (vg0 (#) (x `| Z))) by A37, A38, A39, A49, VALUED_1:def_1;
then A60: ( x0 in dom (vf0 (#) (x `| Z)) & x0 in dom (vg0 (#) (x `| Z)) ) by XBOOLE_0:def_4;
then A61: (vf0 (#) (x `| Z)) . x0 = ((Im f) . (R2-to-C . (<:x,y:> . x0))) * ((x `| Z) . x0) by A57, VALUED_1:def_4;
A62: (vg0 (#) (x `| Z)) . x0 = ((Im g) . (R2-to-C . (<:x,y:> . x0))) * ((x `| Z) . x0) by A59, A60, VALUED_1:def_4;
(v0 (#) (x `| Z)) . x0 = (v0 . x0) * ((x `| Z) . x0) by A49, VALUED_1:def_4
.= (((Im f) . (R2-to-C . (<:x,y:> . x0))) + ((Im g) . (R2-to-C . (<:x,y:> . x0)))) * ((x `| Z) . x0) by A53, A54, VALUED_1:def_1
.= ((vf0 (#) (x `| Z)) . x0) + ((vg0 (#) (x `| Z)) . x0) by A62, A61
.= ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0 by A37, A38, A39, A49, VALUED_1:def_1 ;
hence  (v0 (#) (x `| Z)) . x0 = ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0 ; ::_thesis: verum
end;
hence  v0 (#) (x `| Z) = (vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z)) by A37, A38, A39, FUNCT_1:2; ::_thesis: verum
end;
A63: u0 (#) (y `| Z) = (uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))
proof
A64: dom ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) = (dom (uf0 (#) (y `| Z))) /\ (dom (ug0 (#) (y `| Z))) by VALUED_1:def_1
.= ((dom uf0) /\ (dom (y `| Z))) /\ (dom (ug0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom uf0) /\ (dom (y `| Z))) /\ ((dom ug0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom uf0) /\ ((dom (y `| Z)) /\ ((dom ug0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom uf0) /\ (((dom (y `| Z)) /\ (dom (y `| Z))) /\ (dom ug0)) by XBOOLE_1:16
.= ((dom uf0) /\ (dom ug0)) /\ (dom (y `| Z)) by XBOOLE_1:16 ;
A65: dom (u0 (#) (y `| Z)) = (dom u0) /\ (dom (y `| Z)) by VALUED_1:def_4;
A66: dom u0 = (dom uf0) /\ (dom ug0)
proof
A67: for x0 being set st x0 in dom u0 holds
x0 in (dom uf0) /\ (dom ug0)
proof
let x0 be set ; ::_thesis: ( x0 in dom u0 implies x0 in (dom uf0) /\ (dom ug0) )
assume A68: x0 in dom u0 ; ::_thesis: x0 in (dom uf0) /\ (dom ug0)
A69: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C) ) by A68, A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A70: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) ) by A69, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g)) by MESFUN6C:5;
then  R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g)) by VALUED_1:def_1;
then  ( R2-to-C . (<:x,y:> . x0) in dom (Re f) & R2-to-C . (<:x,y:> . x0) in dom (Re g) ) by XBOOLE_0:def_4;
then  ( <:x,y:> . x0 in dom ((Re f) * R2-to-C) & <:x,y:> . x0 in dom ((Re g) * R2-to-C) ) by A70, FUNCT_1:11;
then  ( x0 in dom uf0 & x0 in dom ug0 ) by A3, A4, A69, FUNCT_1:11;
hence  x0 in (dom uf0) /\ (dom ug0) by XBOOLE_0:def_4; ::_thesis: verum
end;
 for x0 being set st x0 in (dom uf0) /\ (dom ug0) holds
x0 in dom u0
proof
let x0 be set ; ::_thesis: ( x0 in (dom uf0) /\ (dom ug0) implies x0 in dom u0 )
assume A71: x0 in (dom uf0) /\ (dom ug0) ; ::_thesis: x0 in dom u0
A72: ( x0 in dom uf0 & x0 in dom ug0 ) by A71, XBOOLE_0:def_4;
then A73: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A74: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re g) * R2-to-C) ) by A72, A4, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A75: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re f) ) by A73, FUNCT_1:11;
 ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re g) ) by A74, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g)) by A75, XBOOLE_0:def_4;
then  R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g)) by VALUED_1:def_1;
then  R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) by MESFUN6C:5;
then  <:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C) by A75, FUNCT_1:11;
hence  x0 in dom u0 by A8, A73, FUNCT_1:11; ::_thesis: verum
end;
hence  dom u0 = (dom uf0) /\ (dom ug0) by A67, TARSKI:1; ::_thesis: verum
end;
 for x0 being set st x0 in dom (u0 (#) (y `| Z)) holds
(u0 (#) (y `| Z)) . x0 = ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (u0 (#) (y `| Z)) implies (u0 (#) (y `| Z)) . x0 = ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0 )
assume A76: x0 in dom (u0 (#) (y `| Z)) ; ::_thesis: (u0 (#) (y `| Z)) . x0 = ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0
 x0 in (dom u0) /\ (dom (y `| Z)) by A76, VALUED_1:def_4;
then A77: ( x0 in dom u0 & x0 in dom (y `| Z) ) by XBOOLE_0:def_4;
then A78: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C) ) by A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A79: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) ) by A78, FUNCT_1:11;
set c0 = R2-to-C . (<:x,y:> . x0);
A80: u0 . x0 = ((Re (f + g)) * R2-to-C) . (<:x,y:> . x0) by A8, A77, FUNCT_1:12
.= (Re (f + g)) . (R2-to-C . (<:x,y:> . x0)) by A78, FUNCT_1:12
.= ((Re f) + (Re g)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:5 ;
A81: R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g)) by A79, MESFUN6C:5;
A82: ( x0 in dom uf0 & x0 in dom ug0 ) by A66, A77, XBOOLE_0:def_4;
then A83: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A84: uf0 . x0 = ((Re f) * R2-to-C) . (<:x,y:> . x0) by A3, A82, FUNCT_1:12
.= (Re f) . (R2-to-C . (<:x,y:> . x0)) by A83, FUNCT_1:12 ;
A85: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re g) * R2-to-C) ) by A4, A82, FUNCT_1:11;
A86: ug0 . x0 = ((Re g) * R2-to-C) . (<:x,y:> . x0) by A4, A82, FUNCT_1:12
.= (Re g) . (R2-to-C . (<:x,y:> . x0)) by A85, FUNCT_1:12 ;
 x0 in (dom (uf0 (#) (y `| Z))) /\ (dom (ug0 (#) (y `| Z))) by A64, A65, A66, A76, VALUED_1:def_1;
then A87: ( x0 in dom (uf0 (#) (y `| Z)) & x0 in dom (ug0 (#) (y `| Z)) ) by XBOOLE_0:def_4;
then A88: (uf0 (#) (y `| Z)) . x0 = ((Re f) . (R2-to-C . (<:x,y:> . x0))) * ((y `| Z) . x0) by A84, VALUED_1:def_4;
A89: (ug0 (#) (y `| Z)) . x0 = ((Re g) . (R2-to-C . (<:x,y:> . x0))) * ((y `| Z) . x0) by A86, A87, VALUED_1:def_4;
(u0 (#) (y `| Z)) . x0 = (u0 . x0) * ((y `| Z) . x0) by A76, VALUED_1:def_4
.= (((Re f) . (R2-to-C . (<:x,y:> . x0))) + ((Re g) . (R2-to-C . (<:x,y:> . x0)))) * ((y `| Z) . x0) by A80, A81, VALUED_1:def_1
.= ((uf0 (#) (y `| Z)) . x0) + ((ug0 (#) (y `| Z)) . x0) by A89, A88
.= ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0 by A64, A65, A66, A76, VALUED_1:def_1 ;
hence  (u0 (#) (y `| Z)) . x0 = ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0 ; ::_thesis: verum
end;
hence  u0 (#) (y `| Z) = (uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z)) by A64, A65, A66, FUNCT_1:2; ::_thesis: verum
end;
A90: v0 (#) (y `| Z) = (vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))
proof
A91: dom ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) = (dom (vf0 (#) (y `| Z))) /\ (dom (vg0 (#) (y `| Z))) by VALUED_1:def_1
.= ((dom vf0) /\ (dom (y `| Z))) /\ (dom (vg0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom vf0) /\ (dom (y `| Z))) /\ ((dom vg0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom vf0) /\ ((dom (y `| Z)) /\ ((dom vg0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom vf0) /\ (((dom (y `| Z)) /\ (dom (y `| Z))) /\ (dom vg0)) by XBOOLE_1:16
.= ((dom vf0) /\ (dom vg0)) /\ (dom (y `| Z)) by XBOOLE_1:16 ;
A92: dom (v0 (#) (y `| Z)) = (dom v0) /\ (dom (y `| Z)) by VALUED_1:def_4;
A93: dom v0 = (dom vf0) /\ (dom vg0)
proof
A94: for x0 being set st x0 in dom v0 holds
x0 in (dom vf0) /\ (dom vg0)
proof
let x0 be set ; ::_thesis: ( x0 in dom v0 implies x0 in (dom vf0) /\ (dom vg0) )
assume A95: x0 in dom v0 ; ::_thesis: x0 in (dom vf0) /\ (dom vg0)
A96: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C) ) by A8, A95, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A97: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) ) by A96, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g)) by MESFUN6C:5;
then  R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g)) by VALUED_1:def_1;
then  ( R2-to-C . (<:x,y:> . x0) in dom (Im f) & R2-to-C . (<:x,y:> . x0) in dom (Im g) ) by XBOOLE_0:def_4;
then  ( <:x,y:> . x0 in dom ((Im f) * R2-to-C) & <:x,y:> . x0 in dom ((Im g) * R2-to-C) ) by A97, FUNCT_1:11;
then  ( x0 in dom vf0 & x0 in dom vg0 ) by A3, A4, A96, FUNCT_1:11;
hence  x0 in (dom vf0) /\ (dom vg0) by XBOOLE_0:def_4; ::_thesis: verum
end;
 for x0 being set st x0 in (dom vf0) /\ (dom vg0) holds
x0 in dom v0
proof
let x0 be set ; ::_thesis: ( x0 in (dom vf0) /\ (dom vg0) implies x0 in dom v0 )
assume A98: x0 in (dom vf0) /\ (dom vg0) ; ::_thesis: x0 in dom v0
A99: ( x0 in dom vf0 & x0 in dom vg0 ) by A98, XBOOLE_0:def_4;
then A100: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A101: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im g) * R2-to-C) ) by A99, A4, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A102: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im f) ) by A100, FUNCT_1:11;
 ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im g) ) by A101, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g)) by A102, XBOOLE_0:def_4;
then  R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g)) by VALUED_1:def_1;
then  R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) by MESFUN6C:5;
then  <:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C) by A102, FUNCT_1:11;
hence  x0 in dom v0 by A8, A100, FUNCT_1:11; ::_thesis: verum
end;
hence  dom v0 = (dom vf0) /\ (dom vg0) by A94, TARSKI:1; ::_thesis: verum
end;
 for x0 being set st x0 in dom (v0 (#) (y `| Z)) holds
(v0 (#) (y `| Z)) . x0 = ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (v0 (#) (y `| Z)) implies (v0 (#) (y `| Z)) . x0 = ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0 )
assume A103: x0 in dom (v0 (#) (y `| Z)) ; ::_thesis: (v0 (#) (y `| Z)) . x0 = ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0
 x0 in (dom v0) /\ (dom (y `| Z)) by A103, VALUED_1:def_4;
then A104: ( x0 in dom v0 & x0 in dom (y `| Z) ) by XBOOLE_0:def_4;
then A105: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C) ) by A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A106: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) ) by A105, FUNCT_1:11;
set c0 = R2-to-C . (<:x,y:> . x0);
A107: v0 . x0 = ((Im (f + g)) * R2-to-C) . (<:x,y:> . x0) by A8, A104, FUNCT_1:12
.= (Im (f + g)) . (R2-to-C . (<:x,y:> . x0)) by A105, FUNCT_1:12
.= ((Im f) + (Im g)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:5 ;
A108: R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g)) by A106, MESFUN6C:5;
A109: ( x0 in dom vf0 & x0 in dom vg0 ) by A93, A104, XBOOLE_0:def_4;
then A110: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A111: vf0 . x0 = ((Im f) * R2-to-C) . (<:x,y:> . x0) by A3, A109, FUNCT_1:12
.= (Im f) . (R2-to-C . (<:x,y:> . x0)) by A110, FUNCT_1:12 ;
A112: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im g) * R2-to-C) ) by A4, A109, FUNCT_1:11;
A113: vg0 . x0 = ((Im g) * R2-to-C) . (<:x,y:> . x0) by A4, A109, FUNCT_1:12
.= (Im g) . (R2-to-C . (<:x,y:> . x0)) by A112, FUNCT_1:12 ;
 x0 in (dom (vf0 (#) (y `| Z))) /\ (dom (vg0 (#) (y `| Z))) by A91, A92, A93, A103, VALUED_1:def_1;
then A114: ( x0 in dom (vf0 (#) (y `| Z)) & x0 in dom (vg0 (#) (y `| Z)) ) by XBOOLE_0:def_4;
then A115: (vf0 (#) (y `| Z)) . x0 = ((Im f) . (R2-to-C . (<:x,y:> . x0))) * ((y `| Z) . x0) by A111, VALUED_1:def_4;
A116: (vg0 (#) (y `| Z)) . x0 = ((Im g) . (R2-to-C . (<:x,y:> . x0))) * ((y `| Z) . x0) by A113, A114, VALUED_1:def_4;
(v0 (#) (y `| Z)) . x0 = (v0 . x0) * ((y `| Z) . x0) by A103, VALUED_1:def_4
.= (((Im f) . (R2-to-C . (<:x,y:> . x0))) + ((Im g) . (R2-to-C . (<:x,y:> . x0)))) * ((y `| Z) . x0) by A107, A108, VALUED_1:def_1
.= ((vf0 (#) (y `| Z)) . x0) + ((vg0 (#) (y `| Z)) . x0) by A116, A115
.= ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0 by A91, A92, A93, A103, VALUED_1:def_1 ;
hence  (v0 (#) (y `| Z)) . x0 = ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0 ; ::_thesis: verum
end;
hence  v0 (#) (y `| Z) = (vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z)) by A91, A92, A93, FUNCT_1:2; ::_thesis: verum
end;
A117: [.a,b.] c= dom uf0
proof
 for x0 being set st x0 in [.a,b.] holds
x0 in dom uf0
proof
let x0 be set ; ::_thesis: ( x0 in [.a,b.] implies x0 in dom uf0 )
assume A118: x0 in [.a,b.] ; ::_thesis: x0 in dom uf0
A119: C . x0 in rng C by A2, A118, FUNCT_1:3;
A120: ( x0 in dom x & x0 in dom y ) by A2, A118;
A121: x0 in (dom x) /\ (dom y) by A118, A2, XBOOLE_0:def_4;
then A122: x0 in dom <:x,y:> by FUNCT_3:def_7;
set R2 = <:x,y:> . x0;
 <:x,y:> . x0 = [(x . x0),(y . x0)] by A121, FUNCT_3:48;
then  <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def_2;
then A123: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def_1;
 x0 in dom (<i> (#) y) by A120, VALUED_1:def_5;
then  x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A118, XBOOLE_0:def_4;
then A124: x0 in dom (x + (<i> (#) y)) by VALUED_1:def_1;
A125: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def_2;
A126: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A118, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A124, VALUED_1:def_1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A125, A126, Def1
.= R2-to-C . (<:x,y:> . x0) by A121, FUNCT_3:48 ;
then  R2-to-C . (<:x,y:> . x0) in dom f by A1, A119;
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 A123, FUNCT_1:11;
hence  x0 in dom uf0 by A3, A122, FUNCT_1:11; ::_thesis: verum
end;
hence  [.a,b.] c= dom uf0 by TARSKI:def_3; ::_thesis: verum
end;
A127: [.a,b.] c= dom vf0
proof
 for x0 being set st x0 in [.a,b.] holds
x0 in dom vf0
proof
let x0 be set ; ::_thesis: ( x0 in [.a,b.] implies x0 in dom vf0 )
assume A128: x0 in [.a,b.] ; ::_thesis: x0 in dom vf0
A129: C . x0 in rng C by A2, A128, FUNCT_1:3;
A130: ( x0 in dom x & x0 in dom y ) by A2, A128;
A131: x0 in (dom x) /\ (dom y) by A2, A128, XBOOLE_0:def_4;
then A132: x0 in dom <:x,y:> by FUNCT_3:def_7;
set R2 = <:x,y:> . x0;
 <:x,y:> . x0 = [(x . x0),(y . x0)] by A131, FUNCT_3:48;
then  <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def_2;
then A133: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def_1;
 x0 in dom (<i> (#) y) by A130, VALUED_1:def_5;
then  x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A128, XBOOLE_0:def_4;
then A134: x0 in dom (x + (<i> (#) y)) by VALUED_1:def_1;
A135: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def_2;
A136: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A128, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A134, VALUED_1:def_1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A135, A136, Def1
.= R2-to-C . (<:x,y:> . x0) by A131, FUNCT_3:48 ;
then  R2-to-C . (<:x,y:> . x0) in dom f by A1, A129;
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 A133, FUNCT_1:11;
hence  x0 in dom vf0 by A3, A132, FUNCT_1:11; ::_thesis: verum
end;
hence  [.a,b.] c= dom vf0 by TARSKI:def_3; ::_thesis: verum
end;
A137: [.a,b.] c= dom ug0
proof
 for x0 being set st x0 in [.a,b.] holds
x0 in dom ug0
proof
let x0 be set ; ::_thesis: ( x0 in [.a,b.] implies x0 in dom ug0 )
assume A138: x0 in [.a,b.] ; ::_thesis: x0 in dom ug0
A139: C . x0 in rng C by A138, A2, FUNCT_1:3;
A140: ( x0 in dom x & x0 in dom y ) by A2, A138;
A141: x0 in (dom x) /\ (dom y) by A2, A138, XBOOLE_0:def_4;
then A142: x0 in dom <:x,y:> by FUNCT_3:def_7;
set R2 = <:x,y:> . x0;
 <:x,y:> . x0 = [(x . x0),(y . x0)] by A141, FUNCT_3:48;
then  <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def_2;
then A143: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def_1;
 x0 in dom (<i> (#) y) by A140, VALUED_1:def_5;
then  x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A138, XBOOLE_0:def_4;
then A144: x0 in dom (x + (<i> (#) y)) by VALUED_1:def_1;
A145: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def_2;
A146: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A138, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A144, VALUED_1:def_1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A145, A146, Def1
.= R2-to-C . (<:x,y:> . x0) by A141, FUNCT_3:48 ;
then  R2-to-C . (<:x,y:> . x0) in dom g by A1, A139;
then  R2-to-C . (<:x,y:> . x0) in dom (Re g) by COMSEQ_3:def_3;
then  <:x,y:> . x0 in dom ((Re g) * R2-to-C) by A143, FUNCT_1:11;
hence  x0 in dom ug0 by A4, A142, FUNCT_1:11; ::_thesis: verum
end;
hence  [.a,b.] c= dom ug0 by TARSKI:def_3; ::_thesis: verum
end;
A147: [.a,b.] c= dom vg0
proof
 for x0 being set st x0 in [.a,b.] holds
x0 in dom vg0
proof
let x0 be set ; ::_thesis: ( x0 in [.a,b.] implies x0 in dom vg0 )
assume A148: x0 in [.a,b.] ; ::_thesis: x0 in dom vg0
A149: C . x0 in rng C by A2, A148, FUNCT_1:3;
A150: ( x0 in dom x & x0 in dom y ) by A2, A148;
A151: x0 in (dom x) /\ (dom y) by A148, A2, XBOOLE_0:def_4;
then A152: x0 in dom <:x,y:> by FUNCT_3:def_7;
set R2 = <:x,y:> . x0;
 <:x,y:> . x0 = [(x . x0),(y . x0)] by A151, FUNCT_3:48;
then  <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def_2;
then A153: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def_1;
 x0 in dom (<i> (#) y) by A150, VALUED_1:def_5;
then  x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A148, XBOOLE_0:def_4;
then A154: x0 in dom (x + (<i> (#) y)) by VALUED_1:def_1;
A155: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def_2;
A156: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A148, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A154, VALUED_1:def_1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A155, A156, Def1
.= R2-to-C . (<:x,y:> . x0) by A151, FUNCT_3:48 ;
then  R2-to-C . (<:x,y:> . x0) in dom g by A1, A149;
then  R2-to-C . (<:x,y:> . x0) in dom (Im g) by COMSEQ_3:def_4;
then  <:x,y:> . x0 in dom ((Im g) * R2-to-C) by A153, FUNCT_1:11;
hence  x0 in dom vg0 by A4, A152, FUNCT_1:11; ::_thesis: verum
end;
hence  [.a,b.] c= dom vg0 by TARSKI:def_3; ::_thesis: verum
end;
A157: ['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))
proof
A158: ['a,b'] = [.a,b.] by A2, INTEGRA5:def_3;
A159: dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) = (dom (uf0 (#) (x `| Z))) /\ (dom (vf0 (#) (y `| Z))) by VALUED_1:12
.= ((dom uf0) /\ (dom (x `| Z))) /\ (dom (vf0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom uf0) /\ (dom (x `| Z))) /\ ((dom vf0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom uf0) /\ ((dom (x `| Z)) /\ ((dom vf0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom uf0) /\ (Z /\ ((dom (y `| Z)) /\ (dom vf0))) by A2, FDIFF_1:def_7
.= (dom uf0) /\ (Z /\ (Z /\ (dom vf0))) by A2, FDIFF_1:def_7
.= (dom uf0) /\ ((Z /\ Z) /\ (dom vf0)) by XBOOLE_1:16
.= ((dom uf0) /\ (dom vf0)) /\ Z by XBOOLE_1:16 ;
 [.a,b.] c= (dom uf0) /\ (dom vf0) by A117, A127, XBOOLE_1:19;
hence  ['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) by A2, A158, A159, XBOOLE_1:19; ::_thesis: verum
end;
A160: ['a,b'] c= dom ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z)))
proof
A161: ['a,b'] = [.a,b.] by A2, INTEGRA5:def_3;
A162: dom ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))) = (dom (ug0 (#) (x `| Z))) /\ (dom (vg0 (#) (y `| Z))) by VALUED_1:12
.= ((dom ug0) /\ (dom (x `| Z))) /\ (dom (vg0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom ug0) /\ (dom (x `| Z))) /\ ((dom vg0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom ug0) /\ ((dom (x `| Z)) /\ ((dom vg0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom ug0) /\ (Z /\ ((dom (y `| Z)) /\ (dom vg0))) by A2, FDIFF_1:def_7
.= (dom ug0) /\ (Z /\ (Z /\ (dom vg0))) by A2, FDIFF_1:def_7
.= (dom ug0) /\ ((Z /\ Z) /\ (dom vg0)) by XBOOLE_1:16
.= ((dom ug0) /\ (dom vg0)) /\ Z by XBOOLE_1:16 ;
 [.a,b.] c= (dom ug0) /\ (dom vg0) by A137, A147, XBOOLE_1:19;
hence  ['a,b'] c= dom ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))) by A2, A161, A162, XBOOLE_1:19; ::_thesis: verum
end;
A163: ['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))
proof
A164: ['a,b'] = [.a,b.] by A2, INTEGRA5:def_3;
A165: dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) = (dom (vf0 (#) (x `| Z))) /\ (dom (uf0 (#) (y `| Z))) by VALUED_1:def_1
.= ((dom vf0) /\ (dom (x `| Z))) /\ (dom (uf0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom vf0) /\ (dom (x `| Z))) /\ ((dom uf0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom vf0) /\ ((dom (x `| Z)) /\ ((dom uf0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom vf0) /\ (Z /\ ((dom (y `| Z)) /\ (dom uf0))) by A2, FDIFF_1:def_7
.= (dom vf0) /\ (Z /\ (Z /\ (dom uf0))) by A2, FDIFF_1:def_7
.= (dom vf0) /\ ((Z /\ Z) /\ (dom uf0)) by XBOOLE_1:16
.= ((dom vf0) /\ (dom uf0)) /\ Z by XBOOLE_1:16 ;
 [.a,b.] c= (dom vf0) /\ (dom uf0) by A117, A127, XBOOLE_1:19;
hence  ['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) by A2, A164, A165, XBOOLE_1:19; ::_thesis: verum
end;
A166: ['a,b'] c= dom ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z)))
proof
A167: ['a,b'] = [.a,b.] by A2, INTEGRA5:def_3;
A168: dom ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z))) = (dom (vg0 (#) (x `| Z))) /\ (dom (ug0 (#) (y `| Z))) by VALUED_1:def_1
.= ((dom vg0) /\ (dom (x `| Z))) /\ (dom (ug0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom vg0) /\ (dom (x `| Z))) /\ ((dom ug0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom vg0) /\ ((dom (x `| Z)) /\ ((dom ug0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom vg0) /\ (Z /\ ((dom (y `| Z)) /\ (dom ug0))) by A2, FDIFF_1:def_7
.= (dom vg0) /\ (Z /\ (Z /\ (dom ug0))) by A2, FDIFF_1:def_7
.= (dom vg0) /\ ((Z /\ Z) /\ (dom ug0)) by XBOOLE_1:16
.= ((dom vg0) /\ (dom ug0)) /\ Z by XBOOLE_1:16 ;
 [.a,b.] c= (dom ug0) /\ (dom vg0) by A137, A147, XBOOLE_1:19;
hence  ['a,b'] c= dom ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z))) by A2, A167, A168, XBOOLE_1:19; ::_thesis: verum
end;
A169: (uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A170: (ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A171: (vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A172: (vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A173: ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
A174: ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
A175: ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
A176: ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
integral ((f + g),C) = (integral ((((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) - ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z)))),a,b)) + ((integral ((((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) + ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z)))),a,b)) * <i>) by A36, A63, A9, A90, A8, A2, A6, A7, Def4
.= (integral (((((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) - (vf0 (#) (y `| Z))) - (vg0 (#) (y `| Z))),a,b)) + ((integral ((((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) + ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z)))),a,b)) * <i>) by RFUNCT_1:20
.= (integral (((((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) - (vf0 (#) (y `| Z))) - (vg0 (#) (y `| Z))),a,b)) + ((integral (((((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) + (uf0 (#) (y `| Z))) + (ug0 (#) (y `| Z))),a,b)) * <i>) by RFUNCT_1:8
.= (integral (((((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) + (ug0 (#) (x `| Z))) - (vg0 (#) (y `| Z))),a,b)) + ((integral (((((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) + (uf0 (#) (y `| Z))) + (ug0 (#) (y `| Z))),a,b)) * <i>) by RFUNCT_1:8
.= (integral (((((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) + (ug0 (#) (x `| Z))) - (vg0 (#) (y `| Z))),a,b)) + ((integral (((((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) + (vg0 (#) (x `| Z))) + (ug0 (#) (y `| Z))),a,b)) * <i>) by RFUNCT_1:8
.= (integral ((((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) + ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z)))),a,b)) + ((integral (((((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) + (vg0 (#) (x `| Z))) + (ug0 (#) (y `| Z))),a,b)) * <i>) by RFUNCT_1:8
.= (integral ((((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) + ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z)))),a,b)) + ((integral ((((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) + ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z)))),a,b)) * <i>) by RFUNCT_1:8
.= ((integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + (integral (((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))),a,b))) + ((integral ((((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) + ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z)))),a,b)) * <i>) by A2, A157, A160, A169, A170, A173, A174, INTEGRA6:12
.= ((integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + (integral (((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))),a,b))) + (((integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b)) + (integral (((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z))),a,b))) * <i>) by A2, A163, A166, A171, A172, A175, A176, INTEGRA6:12
.= (integral (f,C)) + (integral (g,C)) by A4, A5, A3 ;
hence  integral ((f + g),C) = (integral (f,C)) + (integral (g,C)) ; ::_thesis: verum
end;

theorem :: INTEGR1C:2
for f being PartFunc of COMPLEX,COMPLEX
for C being C1-curve st rng C c= dom f & f is_integrable_on C & f is_bounded_on C holds
for r being Real holds integral ((r (#) f),C) = r * (integral (f,C))
proof
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for C being C1-curve st rng C c= dom f & f is_integrable_on C & f is_bounded_on C holds
for r being Real holds integral ((r (#) f),C) = r * (integral (f,C))
let C be C1-curve; ::_thesis: ( rng C c= dom f & f is_integrable_on C & f is_bounded_on C implies for r being Real holds integral ((r (#) f),C) = r * (integral (f,C)) )
assume A1: ( rng C c= dom f & f is_integrable_on C & f is_bounded_on C ) ; ::_thesis: for r being Real holds integral ((r (#) f),C) = r * (integral (f,C))
let r be Real; ::_thesis: integral ((r (#) f),C) = r * (integral (f,C))
consider a, b being Real, x, y being PartFunc of REAL,REAL, Z being Subset of REAL such that
A2: ( a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & x `| Z is continuous & y `| Z is continuous & C = (x + (<i> (#) y)) | [.a,b.] ) by Def3;
consider uf0, vf0 being PartFunc of REAL,REAL such that
A3: ( uf0 = ((Re f) * R2-to-C) * <:x,y:> & vf0 = ((Im f) * R2-to-C) * <:x,y:> & integral (f,x,y,a,b,Z) = (integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + ((integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b)) * <i>) ) by Def2;
A4: dom (r (#) f) = dom f by VALUED_1:def_5;
consider u0, v0 being PartFunc of REAL,REAL such that
A5: ( u0 = ((Re (r (#) f)) * R2-to-C) * <:x,y:> & v0 = ((Im (r (#) f)) * R2-to-C) * <:x,y:> & integral ((r (#) 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;
A6: dom u0 = dom uf0
proof
A7: for x0 being set st x0 in dom u0 holds
x0 in dom uf0
proof
let x0 be set ; ::_thesis: ( x0 in dom u0 implies x0 in dom uf0 )
assume A8: x0 in dom u0 ; ::_thesis: x0 in dom uf0
A9: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) ) by A5, A8, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A10: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re (r (#) f)) ) by A9, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom (r (#) (Re f)) by MESFUN6C:2;
then  R2-to-C . (<:x,y:> . x0) in dom (Re f) by VALUED_1:def_5;
then  <:x,y:> . x0 in dom ((Re f) * R2-to-C) by A10, FUNCT_1:11;
hence  x0 in dom uf0 by A3, A9, FUNCT_1:11; ::_thesis: verum
end;
 for x0 being set st x0 in dom uf0 holds
x0 in dom u0
proof
let x0 be set ; ::_thesis: ( x0 in dom uf0 implies x0 in dom u0 )
assume A11: x0 in dom uf0 ; ::_thesis: x0 in dom u0
A12: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, A11, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A13: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Re f) ) by A12, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom (r (#) (Re f)) by VALUED_1:def_5;
then  R2-to-C . (<:x,y:> . x0) in dom (Re (r (#) f)) by MESFUN6C:2;
then  <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) by A13, FUNCT_1:11;
hence  x0 in dom u0 by A5, A12, FUNCT_1:11; ::_thesis: verum
end;
hence  dom u0 = dom uf0 by A7, TARSKI:1; ::_thesis: verum
end;
A14: dom v0 = dom vf0
proof
A15: for x0 being set st x0 in dom v0 holds
x0 in dom vf0
proof
let x0 be set ; ::_thesis: ( x0 in dom v0 implies x0 in dom vf0 )
assume A16: x0 in dom v0 ; ::_thesis: x0 in dom vf0
A17: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) ) by A16, A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A18: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im (r (#) f)) ) by A17, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom (r (#) (Im f)) by MESFUN6C:2;
then  R2-to-C . (<:x,y:> . x0) in dom (Im f) by VALUED_1:def_5;
then  <:x,y:> . x0 in dom ((Im f) * R2-to-C) by A18, FUNCT_1:11;
hence  x0 in dom vf0 by A3, A17, FUNCT_1:11; ::_thesis: verum
end;
 for x0 being set st x0 in dom vf0 holds
x0 in dom v0
proof
let x0 be set ; ::_thesis: ( x0 in dom vf0 implies x0 in dom v0 )
assume A19: x0 in dom vf0 ; ::_thesis: x0 in dom v0
A20: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A19, A3, FUNCT_1:11;
set R2 = <:x,y:> . x0;
A21: ( <:x,y:> . x0 in dom R2-to-C & R2-to-C . (<:x,y:> . x0) in dom (Im f) ) by A20, FUNCT_1:11;
then  R2-to-C . (<:x,y:> . x0) in dom (r (#) (Im f)) by VALUED_1:def_5;
then  R2-to-C . (<:x,y:> . x0) in dom (Im (r (#) f)) by MESFUN6C:2;
then  <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) by A21, FUNCT_1:11;
hence  x0 in dom v0 by A5, A20, FUNCT_1:11; ::_thesis: verum
end;
hence  dom v0 = dom vf0 by A15, TARSKI:1; ::_thesis: verum
end;
A22: u0 (#) (x `| Z) = r (#) (uf0 (#) (x `| Z))
proof
A23: dom (r (#) (uf0 (#) (x `| Z))) = dom (uf0 (#) (r (#) (x `| Z))) by RFUNCT_1:13
.= (dom uf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def_4
.= (dom uf0) /\ (dom (x `| Z)) by VALUED_1:def_5 ;
A24: dom (u0 (#) (x `| Z)) = (dom u0) /\ (dom (x `| Z)) by VALUED_1:def_4;
A25: dom (u0 (#) (x `| Z)) = dom (r (#) (uf0 (#) (x `| Z))) by A6, A23, VALUED_1:def_4;
 for x0 being set st x0 in dom (u0 (#) (x `| Z)) holds
(u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (u0 (#) (x `| Z)) implies (u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0 )
assume A26: x0 in dom (u0 (#) (x `| Z)) ; ::_thesis: (u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0
A27: x0 in (dom u0) /\ (dom (x `| Z)) by A26, VALUED_1:def_4;
then A28: ( x0 in dom u0 & x0 in dom (x `| Z) ) by XBOOLE_0:def_4;
then A29: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A30: u0 . x0 = ((Re (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A28, FUNCT_1:12
.= (Re (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A29, FUNCT_1:12
.= (r (#) (Re f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
 x0 in dom uf0 by A6, A27, XBOOLE_0:def_4;
then A31: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A32: uf0 . x0 = ((Re f) * R2-to-C) . (<:x,y:> . x0) by A3, A6, A28, FUNCT_1:12
.= (Re f) . (R2-to-C . (<:x,y:> . x0)) by A31, FUNCT_1:12 ;
A33: x0 in dom (uf0 (#) (r (#) (x `| Z))) by A26, A25, RFUNCT_1:13;
then  x0 in (dom uf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def_4;
then A34: x0 in dom (r (#) (x `| Z)) by XBOOLE_0:def_4;
(u0 (#) (x `| Z)) . x0 = (u0 . x0) * ((x `| Z) . x0) by A26, VALUED_1:def_4
.= (r * ((Re f) . (R2-to-C . (<:x,y:> . x0)))) * ((x `| Z) . x0) by A30, VALUED_1:6
.= (uf0 . x0) * (r * ((x `| Z) . x0)) by A32
.= (uf0 . x0) * ((r (#) (x `| Z)) . x0) by A34, VALUED_1:def_5
.= (uf0 (#) (r (#) (x `| Z))) . x0 by A33, VALUED_1:def_4
.= (r (#) (uf0 (#) (x `| Z))) . x0 by RFUNCT_1:13 ;
hence  (u0 (#) (x `| Z)) . x0 = (r (#) (uf0 (#) (x `| Z))) . x0 ; ::_thesis: verum
end;
hence  u0 (#) (x `| Z) = r (#) (uf0 (#) (x `| Z)) by A6, A23, A24, FUNCT_1:2; ::_thesis: verum
end;
A35: v0 (#) (x `| Z) = r (#) (vf0 (#) (x `| Z))
proof
A36: dom (r (#) (vf0 (#) (x `| Z))) = dom (vf0 (#) (r (#) (x `| Z))) by RFUNCT_1:13
.= (dom vf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def_4
.= (dom vf0) /\ (dom (x `| Z)) by VALUED_1:def_5 ;
A37: dom (v0 (#) (x `| Z)) = (dom v0) /\ (dom (x `| Z)) by VALUED_1:def_4;
A38: dom (v0 (#) (x `| Z)) = dom (r (#) (vf0 (#) (x `| Z))) by A14, A36, VALUED_1:def_4;
 for x0 being set st x0 in dom (v0 (#) (x `| Z)) holds
(v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (v0 (#) (x `| Z)) implies (v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0 )
assume A39: x0 in dom (v0 (#) (x `| Z)) ; ::_thesis: (v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0
A40: x0 in (dom v0) /\ (dom (x `| Z)) by A39, VALUED_1:def_4;
then A41: ( x0 in dom v0 & x0 in dom (x `| Z) ) by XBOOLE_0:def_4;
then A42: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A43: v0 . x0 = ((Im (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A41, FUNCT_1:12
.= (Im (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A42, FUNCT_1:12
.= (r (#) (Im f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
 x0 in dom vf0 by A14, A40, XBOOLE_0:def_4;
then A44: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A45: vf0 . x0 = ((Im f) * R2-to-C) . (<:x,y:> . x0) by A3, A14, A41, FUNCT_1:12
.= (Im f) . (R2-to-C . (<:x,y:> . x0)) by A44, FUNCT_1:12 ;
A46: x0 in dom (vf0 (#) (r (#) (x `| Z))) by A38, A39, RFUNCT_1:13;
then  x0 in (dom vf0) /\ (dom (r (#) (x `| Z))) by VALUED_1:def_4;
then A47: x0 in dom (r (#) (x `| Z)) by XBOOLE_0:def_4;
(v0 (#) (x `| Z)) . x0 = (v0 . x0) * ((x `| Z) . x0) by A39, VALUED_1:def_4
.= (r * ((Im f) . (R2-to-C . (<:x,y:> . x0)))) * ((x `| Z) . x0) by A43, VALUED_1:6
.= (vf0 . x0) * (r * ((x `| Z) . x0)) by A45
.= (vf0 . x0) * ((r (#) (x `| Z)) . x0) by A47, VALUED_1:def_5
.= (vf0 (#) (r (#) (x `| Z))) . x0 by A46, VALUED_1:def_4
.= (r (#) (vf0 (#) (x `| Z))) . x0 by RFUNCT_1:13 ;
hence  (v0 (#) (x `| Z)) . x0 = (r (#) (vf0 (#) (x `| Z))) . x0 ; ::_thesis: verum
end;
hence  v0 (#) (x `| Z) = r (#) (vf0 (#) (x `| Z)) by A14, A36, A37, FUNCT_1:2; ::_thesis: verum
end;
A48: u0 (#) (y `| Z) = r (#) (uf0 (#) (y `| Z))
proof
A49: dom (r (#) (uf0 (#) (y `| Z))) = dom (uf0 (#) (r (#) (y `| Z))) by RFUNCT_1:13
.= (dom uf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def_4
.= (dom uf0) /\ (dom (y `| Z)) by VALUED_1:def_5 ;
A50: dom (u0 (#) (y `| Z)) = (dom u0) /\ (dom (y `| Z)) by VALUED_1:def_4;
A51: dom (u0 (#) (y `| Z)) = dom (r (#) (uf0 (#) (y `| Z))) by A6, A49, VALUED_1:def_4;
 for x0 being set st x0 in dom (u0 (#) (y `| Z)) holds
(u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (u0 (#) (y `| Z)) implies (u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0 )
assume A52: x0 in dom (u0 (#) (y `| Z)) ; ::_thesis: (u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0
A53: x0 in (dom u0) /\ (dom (y `| Z)) by A52, VALUED_1:def_4;
then A54: ( x0 in dom u0 & x0 in dom (y `| Z) ) by XBOOLE_0:def_4;
then A55: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A56: u0 . x0 = ((Re (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A54, FUNCT_1:12
.= (Re (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A55, FUNCT_1:12
.= (r (#) (Re f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
 x0 in dom uf0 by A6, A53, XBOOLE_0:def_4;
then A57: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Re f) * R2-to-C) ) by A3, FUNCT_1:11;
A58: uf0 . x0 = ((Re f) * R2-to-C) . (<:x,y:> . x0) by A3, A6, A54, FUNCT_1:12
.= (Re f) . (R2-to-C . (<:x,y:> . x0)) by A57, FUNCT_1:12 ;
A59: x0 in dom (uf0 (#) (r (#) (y `| Z))) by A51, A52, RFUNCT_1:13;
then  x0 in (dom uf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def_4;
then A60: x0 in dom (r (#) (y `| Z)) by XBOOLE_0:def_4;
(u0 (#) (y `| Z)) . x0 = (u0 . x0) * ((y `| Z) . x0) by A52, VALUED_1:def_4
.= (r * ((Re f) . (R2-to-C . (<:x,y:> . x0)))) * ((y `| Z) . x0) by A56, VALUED_1:6
.= (uf0 . x0) * (r * ((y `| Z) . x0)) by A58
.= (uf0 . x0) * ((r (#) (y `| Z)) . x0) by A60, VALUED_1:def_5
.= (uf0 (#) (r (#) (y `| Z))) . x0 by A59, VALUED_1:def_4
.= (r (#) (uf0 (#) (y `| Z))) . x0 by RFUNCT_1:13 ;
hence  (u0 (#) (y `| Z)) . x0 = (r (#) (uf0 (#) (y `| Z))) . x0 ; ::_thesis: verum
end;
hence  u0 (#) (y `| Z) = r (#) (uf0 (#) (y `| Z)) by A6, A49, A50, FUNCT_1:2; ::_thesis: verum
end;
A61: v0 (#) (y `| Z) = r (#) (vf0 (#) (y `| Z))
proof
A62: dom (r (#) (vf0 (#) (y `| Z))) = dom (vf0 (#) (r (#) (y `| Z))) by RFUNCT_1:13
.= (dom vf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def_4
.= (dom vf0) /\ (dom (y `| Z)) by VALUED_1:def_5 ;
A63: dom (v0 (#) (y `| Z)) = (dom v0) /\ (dom (y `| Z)) by VALUED_1:def_4;
A64: dom (v0 (#) (y `| Z)) = dom (r (#) (vf0 (#) (y `| Z))) by A14, A62, VALUED_1:def_4;
 for x0 being set st x0 in dom (v0 (#) (y `| Z)) holds
(v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0
proof
let x0 be set ; ::_thesis: ( x0 in dom (v0 (#) (y `| Z)) implies (v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0 )
assume A65: x0 in dom (v0 (#) (y `| Z)) ; ::_thesis: (v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0
A66: x0 in (dom v0) /\ (dom (y `| Z)) by A65, VALUED_1:def_4;
then A67: ( x0 in dom v0 & x0 in dom (y `| Z) ) by XBOOLE_0:def_4;
then A68: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im (r (#) f)) * R2-to-C) ) by A5, FUNCT_1:11;
set R2 = <:x,y:> . x0;
set c0 = R2-to-C . (<:x,y:> . x0);
A69: v0 . x0 = ((Im (r (#) f)) * R2-to-C) . (<:x,y:> . x0) by A5, A67, FUNCT_1:12
.= (Im (r (#) f)) . (R2-to-C . (<:x,y:> . x0)) by A68, FUNCT_1:12
.= (r (#) (Im f)) . (R2-to-C . (<:x,y:> . x0)) by MESFUN6C:2 ;
 x0 in dom vf0 by A14, A66, XBOOLE_0:def_4;
then A70: ( x0 in dom <:x,y:> & <:x,y:> . x0 in dom ((Im f) * R2-to-C) ) by A3, FUNCT_1:11;
A71: vf0 . x0 = ((Im f) * R2-to-C) . (<:x,y:> . x0) by A3, A14, A67, FUNCT_1:12
.= (Im f) . (R2-to-C . (<:x,y:> . x0)) by A70, FUNCT_1:12 ;
A72: x0 in dom (vf0 (#) (r (#) (y `| Z))) by A64, A65, RFUNCT_1:13;
then  x0 in (dom vf0) /\ (dom (r (#) (y `| Z))) by VALUED_1:def_4;
then A73: x0 in dom (r (#) (y `| Z)) by XBOOLE_0:def_4;
(v0 (#) (y `| Z)) . x0 = (v0 . x0) * ((y `| Z) . x0) by A65, VALUED_1:def_4
.= (r * ((Im f) . (R2-to-C . (<:x,y:> . x0)))) * ((y `| Z) . x0) by A69, VALUED_1:6
.= (vf0 . x0) * (r * ((y `| Z) . x0)) by A71
.= (vf0 . x0) * ((r (#) (y `| Z)) . x0) by A73, VALUED_1:def_5
.= (vf0 (#) (r (#) (y `| Z))) . x0 by A72, VALUED_1:def_4
.= (r (#) (vf0 (#) (y `| Z))) . x0 by RFUNCT_1:13 ;
hence  (v0 (#) (y `| Z)) . x0 = (r (#) (vf0 (#) (y `| Z))) . x0 ; ::_thesis: verum
end;
hence  v0 (#) (y `| Z) = r (#) (vf0 (#) (y `| Z)) by A14, A62, A63, FUNCT_1:2; ::_thesis: verum
end;
A74: [.a,b.] c= dom uf0
proof
 for x0 being set st x0 in [.a,b.] holds
x0 in dom uf0
proof
let x0 be set ; ::_thesis: ( x0 in [.a,b.] implies x0 in dom uf0 )
assume A75: x0 in [.a,b.] ; ::_thesis: x0 in dom uf0
A76: C . x0 in rng C by A2, A75, FUNCT_1:3;
A77: ( x0 in dom x & x0 in dom y ) by A2, A75;
A78: x0 in (dom x) /\ (dom y) by A2, A75, XBOOLE_0:def_4;
then A79: x0 in dom <:x,y:> by FUNCT_3:def_7;
set R2 = <:x,y:> . x0;
 <:x,y:> . x0 = [(x . x0),(y . x0)] by A78, FUNCT_3:48;
then  <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def_2;
then A80: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def_1;
 x0 in dom (<i> (#) y) by A77, VALUED_1:def_5;
then  x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A75, XBOOLE_0:def_4;
then A81: x0 in dom (x + (<i> (#) y)) by VALUED_1:def_1;
A82: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def_2;
A83: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A75, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A81, VALUED_1:def_1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A82, A83, Def1
.= R2-to-C . (<:x,y:> . x0) by A78, FUNCT_3:48 ;
then  R2-to-C . (<:x,y:> . x0) in dom f by A1, A76;
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 A80, FUNCT_1:11;
hence  x0 in dom uf0 by A3, A79, FUNCT_1:11; ::_thesis: verum
end;
hence  [.a,b.] c= dom uf0 by TARSKI:def_3; ::_thesis: verum
end;
A84: [.a,b.] c= dom vf0
proof
 for x0 being set st x0 in [.a,b.] holds
x0 in dom vf0
proof
let x0 be set ; ::_thesis: ( x0 in [.a,b.] implies x0 in dom vf0 )
assume A85: x0 in [.a,b.] ; ::_thesis: x0 in dom vf0
A86: C . x0 in rng C by A2, A85, FUNCT_1:3;
A87: ( x0 in dom x & x0 in dom y ) by A2, A85;
A88: x0 in (dom x) /\ (dom y) by A2, A85, XBOOLE_0:def_4;
then A89: x0 in dom <:x,y:> by FUNCT_3:def_7;
set R2 = <:x,y:> . x0;
 <:x,y:> . x0 = [(x . x0),(y . x0)] by A88, FUNCT_3:48;
then  <:x,y:> . x0 in [:REAL,REAL:] by ZFMISC_1:def_2;
then A90: <:x,y:> . x0 in dom R2-to-C by FUNCT_2:def_1;
 x0 in dom (<i> (#) y) by A87, VALUED_1:def_5;
then  x0 in (dom x) /\ (dom (<i> (#) y)) by A2, A85, XBOOLE_0:def_4;
then A91: x0 in dom (x + (<i> (#) y)) by VALUED_1:def_1;
A92: [(x . x0),(y . x0)] in [:REAL,REAL:] by ZFMISC_1:def_2;
A93: ( x . x0 = [(x . x0),(y . x0)] `1 & y . x0 = [(x . x0),(y . x0)] `2 ) ;
C . x0 = (x + (<i> (#) y)) . x0 by A85, A2, FUNCT_1:49
.= (x . x0) + ((<i> (#) y) . x0) by A91, VALUED_1:def_1
.= (x . x0) + (<i> * (y . x0)) by VALUED_1:6
.= R2-to-C . [(x . x0),(y . x0)] by A92, A93, Def1
.= R2-to-C . (<:x,y:> . x0) by A88, FUNCT_3:48 ;
then  R2-to-C . (<:x,y:> . x0) in dom f by A1, A86;
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 A90, FUNCT_1:11;
hence  x0 in dom vf0 by A3, A89, FUNCT_1:11; ::_thesis: verum
end;
hence  [.a,b.] c= dom vf0 by TARSKI:def_3; ::_thesis: verum
end;
A94: ['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))
proof
A95: ['a,b'] = [.a,b.] by A2, INTEGRA5:def_3;
A96: dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) = (dom (uf0 (#) (x `| Z))) /\ (dom (vf0 (#) (y `| Z))) by VALUED_1:12
.= ((dom uf0) /\ (dom (x `| Z))) /\ (dom (vf0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom uf0) /\ (dom (x `| Z))) /\ ((dom vf0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom uf0) /\ ((dom (x `| Z)) /\ ((dom vf0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom uf0) /\ (Z /\ ((dom (y `| Z)) /\ (dom vf0))) by A2, FDIFF_1:def_7
.= (dom uf0) /\ (Z /\ (Z /\ (dom vf0))) by A2, FDIFF_1:def_7
.= (dom uf0) /\ ((Z /\ Z) /\ (dom vf0)) by XBOOLE_1:16
.= ((dom uf0) /\ (dom vf0)) /\ Z by XBOOLE_1:16 ;
 [.a,b.] c= (dom uf0) /\ (dom vf0) by A74, A84, XBOOLE_1:19;
hence  ['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) by A2, A95, A96, XBOOLE_1:19; ::_thesis: verum
end;
A97: ['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))
proof
A98: ['a,b'] = [.a,b.] by A2, INTEGRA5:def_3;
A99: dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) = (dom (vf0 (#) (x `| Z))) /\ (dom (uf0 (#) (y `| Z))) by VALUED_1:def_1
.= ((dom vf0) /\ (dom (x `| Z))) /\ (dom (uf0 (#) (y `| Z))) by VALUED_1:def_4
.= ((dom vf0) /\ (dom (x `| Z))) /\ ((dom uf0) /\ (dom (y `| Z))) by VALUED_1:def_4
.= (dom vf0) /\ ((dom (x `| Z)) /\ ((dom uf0) /\ (dom (y `| Z)))) by XBOOLE_1:16
.= (dom vf0) /\ (Z /\ ((dom (y `| Z)) /\ (dom uf0))) by A2, FDIFF_1:def_7
.= (dom vf0) /\ (Z /\ (Z /\ (dom uf0))) by A2, FDIFF_1:def_7
.= (dom vf0) /\ ((Z /\ Z) /\ (dom uf0)) by XBOOLE_1:16
.= ((dom vf0) /\ (dom uf0)) /\ Z by XBOOLE_1:16 ;
 [.a,b.] c= (dom vf0) /\ (dom uf0) by A74, A84, XBOOLE_1:19;
hence  ['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) by A2, A98, A99, XBOOLE_1:19; ::_thesis: verum
end;
A100: (uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A101: (vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)) is_integrable_on ['a,b'] by A1, A2, Def5;
A102: ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
A103: ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) | ['a,b'] is bounded by A1, A2, Def6;
integral ((r (#) f),C) = (integral (((r (#) (uf0 (#) (x `| Z))) - (r (#) (vf0 (#) (y `| Z)))),a,b)) + ((integral (((r (#) (vf0 (#) (x `| Z))) + (r (#) (uf0 (#) (y `| Z)))),a,b)) * <i>) by A35, A61, A48, A22, A5, A1, A2, A4, Def4
.= (integral ((r (#) ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))),a,b)) + ((integral (((r (#) (vf0 (#) (x `| Z))) + (r (#) (uf0 (#) (y `| Z)))),a,b)) * <i>) by RFUNCT_1:18
.= (integral ((r (#) ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))),a,b)) + ((integral ((r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b)) * <i>) by RFUNCT_1:16
.= (r * (integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b))) + ((integral ((r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b)) * <i>) by A2, A94, A100, A102, INTEGRA6:10
.= (r * (integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b))) + ((r * (integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b))) * <i>) by A2, A97, A101, A103, INTEGRA6:10
.= r * ((integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b)) + ((integral (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))),a,b)) * <i>))
.= r * (integral (f,C)) by A1, A2, A3, Def4 ;
hence  integral ((r (#) f),C) = r * (integral (f,C)) ; ::_thesis: verum
end;

begin

theorem :: INTEGR1C:3
for f being PartFunc of COMPLEX,COMPLEX
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))
proof
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 ) ;
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 ) ;
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) by Def2, A5;
A48: (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 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, XBOOLE_1:1;
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 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 A55: x0 in dom (x | [.a,d.]) ; ::_thesis: (x | [.a,d.]) . x0 = (x1 | [.a,d.]) . x0
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 (<i> (#) y1)) by VALUED_1:def_5;
then A57: x0 in dom (x1 + (<i> (#) 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 (<i> (#) y)) by VALUED_1:def_5;
then A58: x0 in dom (x + (<i> (#) 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 + (<i> (#) y)) . t by A3, A4, A51, A55, A56, FUNCT_1:49;
A61: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A55, A56, FUNCT_1:49;
A62: (x1 + (<i> (#) y1)) . t = (x1 . t) + ((<i> (#) y1) . t) by A57, VALUED_1:def_1
.= (x1 . t) + (<i> * (y1 . t)) by VALUED_1:6 ;
A63: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A58, VALUED_1:def_1
.= (x . t) + (<i> * (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: verum
end;
hence  x | [.a,d.] = x1 | [.a,d.] by A54, FUNCT_1:2; ::_thesis: verum
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 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 A66: x0 in dom (y | [.a,d.]) ; ::_thesis: (y | [.a,d.]) . x0 = (y1 | [.a,d.]) . x0
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 (<i> (#) y1)) by VALUED_1:def_5;
then A68: x0 in dom (x1 + (<i> (#) 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 (<i> (#) y)) by VALUED_1:def_5;
then A69: x0 in dom (x + (<i> (#) 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 + (<i> (#) y)) . t by A3, A4, A51, A66, A67, FUNCT_1:49;
A72: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A66, A67, FUNCT_1:49;
A73: (x1 + (<i> (#) y1)) . t = (x1 . t) + ((<i> (#) y1) . t) by A68, VALUED_1:def_1
.= (x1 . t) + (<i> * (y1 . t)) by VALUED_1:6 ;
A74: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A69, VALUED_1:def_1
.= (x . t) + (<i> * (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: verum
end;
hence  y | [.a,d.] = y1 | [.a,d.] by A65, FUNCT_1:2; ::_thesis: verum
end;
A75: [.a,d.] c= Z by A3, A4, A51, XBOOLE_1:1;
then A76: [.a,d.] c= Z3 by A6, A7, XBOOLE_1:19;
A77: 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 A78: y0 in rng ((x + (<i> (#) y)) | [.a,d.]) ; ::_thesis: y0 in dom f
consider x0 being set  such that
A79: ( x0 in dom ((x + (<i> (#) y)) | [.a,d.]) & y0 = ((x + (<i> (#) y)) | [.a,d.]) . x0 ) by A78, FUNCT_1:def_3;
A80: x0 in (dom (x + (<i> (#) y))) /\ [.a,d.] by A79, 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 A80;
then A81: x0 in dom ((x + (<i> (#) y)) | [.a,b.]) by RELAT_1:61;
then A82: ((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 A79, FUNCT_1:47
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A81, FUNCT_1:47 ;
hence  y0 in dom f by A1, A3, A79, A82; ::_thesis: verum
end;
hence  rng ((x + (<i> (#) y)) | [.a,d.]) c= dom f by TARSKI:def_3; ::_thesis: verum
end;
A83: 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 A84: y0 in rng ((x1 + (<i> (#) y1)) | [.a,d.]) ; ::_thesis: y0 in dom f
consider x0 being set  such that
A85: ( x0 in dom ((x1 + (<i> (#) y1)) | [.a,d.]) & y0 = ((x1 + (<i> (#) y1)) | [.a,d.]) . x0 ) by A84, FUNCT_1:def_3;
 x0 in (dom (x1 + (<i> (#) 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 (<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 A87: ((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 A85;
A88: C . t = (x + (<i> (#) y)) . t by A3, A4, A51, A86, FUNCT_1:49;
A89: C1 . t = (x1 + (<i> (#) y1)) . t by A6, A7, A86, FUNCT_1:49;
((x1 + (<i> (#) y1)) | [.a,d.]) . x0 = (x1 + (<i> (#) y1)) . x0 by A85, FUNCT_1:47
.= (x + (<i> (#) y)) . x0 by A1, A86, A88, A89
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A51, A86, FUNCT_1:49 ;
hence  y0 in dom f by A1, A3, A85, A87; ::_thesis: verum
end;
hence  rng ((x1 + (<i> (#) y1)) | [.a,d.]) c= dom f by TARSKI:def_3; ::_thesis: verum
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, XBOOLE_1:1;
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: verum
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, XBOOLE_1:1;
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 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 A99: x0 in dom (x | [.d,b.]) ; ::_thesis: (x | [.d,b.]) . x0 = (x2 | [.d,b.]) . x0
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 (<i> (#) y2)) by VALUED_1:def_5;
then A101: x0 in dom (x2 + (<i> (#) 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 (<i> (#) y)) by VALUED_1:def_5;
then A102: x0 in dom (x + (<i> (#) 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 + (<i> (#) y)) . t by A3, A4, A95, A99, A100, FUNCT_1:49;
A105: C2 . t = (x2 + (<i> (#) y2)) . t by A12, A13, A99, A100, FUNCT_1:49;
A106: (x2 + (<i> (#) y2)) . t = (x2 . t) + ((<i> (#) y2) . t) by A101, VALUED_1:def_1
.= (x2 . t) + (<i> * (y2 . t)) by VALUED_1:6 ;
A107: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A102, VALUED_1:def_1
.= (x . t) + (<i> * (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: verum
end;
hence  x | [.d,b.] = x2 | [.d,b.] by A98, FUNCT_1:2; ::_thesis: verum
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 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 A110: x0 in dom (y | [.d,b.]) ; ::_thesis: (y | [.d,b.]) . x0 = (y2 | [.d,b.]) . x0
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 (<i> (#) y2)) by VALUED_1:def_5;
then A112: x0 in dom (x2 + (<i> (#) 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 (<i> (#) y)) by VALUED_1:def_5;
then A113: x0 in dom (x + (<i> (#) 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 + (<i> (#) y)) . t by A3, A4, A95, A110, A111, FUNCT_1:49;
A116: C2 . t = (x2 + (<i> (#) y2)) . t by A12, A13, A110, A111, FUNCT_1:49;
A117: (x2 + (<i> (#) y2)) . t = (x2 . t) + ((<i> (#) y2) . t) by A112, VALUED_1:def_1
.= (x2 . t) + (<i> * (y2 . t)) by VALUED_1:6 ;
A118: (x + (<i> (#) y)) . t = (x . t) + ((<i> (#) y) . t) by A113, VALUED_1:def_1
.= (x . t) + (<i> * (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: verum
end;
hence  y | [.d,b.] = y2 | [.d,b.] by A109, FUNCT_1:2; ::_thesis: verum
end;
A119: [.d,b.] c= Z by A3, A4, A95, XBOOLE_1:1;
then A120: [.d,b.] c= Z3 by A12, A13, XBOOLE_1:19;
A121: 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 A122: y0 in rng ((x + (<i> (#) y)) | [.d,b.]) ; ::_thesis: y0 in dom f
consider x0 being set  such that
A123: ( x0 in dom ((x + (<i> (#) y)) | [.d,b.]) & y0 = ((x + (<i> (#) y)) | [.d,b.]) . x0 ) by A122, FUNCT_1:def_3;
A124: x0 in (dom (x + (<i> (#) y))) /\ [.d,b.] by A123, 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 A124;
then A125: x0 in dom ((x + (<i> (#) y)) | [.a,b.]) by RELAT_1:61;
then A126: ((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 A123, FUNCT_1:47
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A125, FUNCT_1:47 ;
hence  y0 in dom f by A1, A3, A123, A126; ::_thesis: verum
end;
hence  rng ((x + (<i> (#) y)) | [.d,b.]) c= dom f by TARSKI:def_3; ::_thesis: verum
end;
A127: 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 A128: y0 in rng ((x2 + (<i> (#) y2)) | [.d,b.]) ; ::_thesis: y0 in dom f
consider x0 being set  such that
A129: ( x0 in dom ((x2 + (<i> (#) y2)) | [.d,b.]) & y0 = ((x2 + (<i> (#) y2)) | [.d,b.]) . x0 ) by A128, FUNCT_1:def_3;
 x0 in (dom (x2 + (<i> (#) 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 (<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 A131: ((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 A129;
A132: C . t = (x + (<i> (#) y)) . t by A3, A4, A95, A130, FUNCT_1:49;
A133: C2 . t = (x2 + (<i> (#) y2)) . t by A12, A13, A130, FUNCT_1:49;
((x2 + (<i> (#) y2)) | [.d,b.]) . x0 = (x2 + (<i> (#) y2)) . x0 by A129, FUNCT_1:47
.= (x + (<i> (#) y)) . x0 by A1, A130, A132, A133
.= ((x + (<i> (#) y)) | [.a,b.]) . x0 by A95, A130, FUNCT_1:49 ;
hence  y0 in dom f by A1, A3, A129, A131; ::_thesis: verum
end;
hence  rng ((x2 + (<i> (#) y2)) | [.d,b.]) c= dom f by TARSKI:def_3; ::_thesis: verum
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, XBOOLE_1:1;
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: 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 A49, A48, A47
.= (integral (f,C1)) + (integral (f,C2)) by A6, A7, A8, A17, Def4, A93 ; ::_thesis: verum
end;