integr1c.miz

begin

 reserve n,n1,m for Element of NAT ;

 reserve r,t,x1 for Real;

 reserve h for 0 -convergent non-zero Real_Sequence;

 reserve c1 for constant Real_Sequence;

 reserve p1 for Real;

 definition

 :: INTEGR1C:def1

 func R2-to-C -> Function of [: REAL , REAL :], COMPLEX means

 : Def1: for p be Element of [: REAL , REAL :], a,b be Element of REAL st a = (p `1 ) & b = (p `2 ) holds (it . [a, b]) = (a + (b * ));

 existence

 proof

 deffunc F( Real, Real) = ($1 + ($2 * ));



 A1: for x be Element of REAL , y be Element of REAL holds F(x,y) in COMPLEX by XCMPLX_0:def 2;

 consider f be Function of [: REAL , REAL :], COMPLEX such that

 A2: for x,y be Element of REAL holds (f . (x,y)) = F(x,y) from FUNCT_7:sch 1( A1);

 deffunc G( Element of [: REAL , REAL :]) = (f . (($1 `1 ),($1 `2 )));

 A3:

 now

 let p be Element of [: REAL , REAL :];

 (p `1 ) is Element of REAL & (p `2 ) is Element of REAL by MCART_1: 10;

 then

 consider a,b be Element of REAL such that

 A4: a = (p `1 ) & b = (p `2 );

 G(p) = (a + (b * )) by A2, A4;

 hence G(p) in COMPLEX by XCMPLX_0:def 2;

 end;

 consider g be Function of [: REAL , REAL :], COMPLEX such that

 A5: for p be Element of [: REAL , REAL :] holds (g . p) = G(p) from FUNCT_2:sch 8( A3);

 take g;

 for p be Element of [: REAL , REAL :], a,b be Element of REAL st a = (p `1 ) & b = (p `2 ) holds (g . [a, b]) = (a + (b * ))

 proof

 let p be Element of [: REAL , REAL :], a,b be Element of REAL such that

 A6: a = (p `1 ) & b = (p `2 );



 A8: [a, b] is Element of [: REAL , REAL :] by ZFMISC_1:def 2;



 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 * )) by A2;

 hence thesis;

 end;

 hence thesis;

 end;

 uniqueness

 proof

 let f,g be Function of [: REAL , REAL :], COMPLEX ;

 assume

 A10: for p be Element of [: REAL , REAL :], a,b be Element of REAL st a = (p `1 ) & b = (p `2 ) holds (f . [a, b]) = (a + (b * ));

 assume

 A11: for p be Element of [: REAL , REAL :], a,b be Element of REAL st a = (p `1 ) & b = (p `2 ) holds (g . [a, b]) = (a + (b * ));

 for p0 be object st p0 in [: REAL , REAL :] holds (f . p0) = (g . p0)

 proof

 let p0 be object;

 assume

 A12: p0 in [: REAL , REAL :];

 then

 consider x0,y0 be object 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;



 A15: (p0 `2 ) = b by A13;



 then (f . p0) = (a + (b * )) by A12, A10, A14, A13

 .= (g . p0) by A13, A12, A11, A14, A15;

 hence thesis;

 end;

 hence f = g by FUNCT_2: 12;

 end;

 end

 definition

 let a,b be Real;

 let x,y be PartFunc of REAL , REAL , Z be Subset of REAL ;

 let f be PartFunc of COMPLEX , COMPLEX ;

 :: INTEGR1C:def2

 func integral (f,x,y,a,b,Z) -> Complex means

 : Def2: ex u0,v0 be 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)) * ));

 existence

 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)) * )) is Complex;

 hence thesis;

 end;

 uniqueness ;

 end

 definition

 let C be PartFunc of REAL , COMPLEX ;

 :: INTEGR1C:def3

 attr C is C1-curve-like means

 : Def3: ex a,b be Real, x,y be PartFunc of REAL , REAL , Z be 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 + ( (#) y)) | [.a, b.]);

 end

 registration

 cluster C1-curve-like for PartFunc of REAL , COMPLEX ;

 existence

 proof

 set a = 1, b = 2;

 set x = cos , y = sin ;

 set Z = ].( - 5), 5.[;

 consider C be PartFunc of REAL , COMPLEX such that

 A1: C = ((x + ( (#) y)) | [.a, b.]);

 take C;



 A2: ( dom (x + ( (#) y))) = REAL by FUNCT_2:def 1;

 ( dom C) = (( dom (x + ( (#) y))) /\ [.a, b.]) by A1, RELAT_1: 61;

 then

 A3: [.a, b.] = ( dom C) by A2, XBOOLE_1: 28;



 A4: Z is open by RCOMP_1: 7;



 A5: [.a, b.] c= Z by XXREAL_1: 47;



 A6: x is_differentiable_on Z by A4, FDIFF_1: 26, SIN_COS: 67;



 A7: y is_differentiable_on Z by A4, FDIFF_1: 26, SIN_COS: 68;

 sin = ( sin | REAL );

 then ( sin | Z) is continuous by FCONT_1: 16;

 then (( - sin ) | Z) is continuous by FCONT_1: 21, SIN_COS: 24;

 then

 A8: ( - ( sin | Z)) is continuous by RFUNCT_1: 46;



 A9: ( dom ( - ( sin | Z))) = ( dom (( - sin ) | Z)) by RFUNCT_1: 46

 .= (( dom ( - sin )) /\ Z) by RELAT_1: 61

 .= ( REAL /\ Z) by SIN_COS: 24, VALUED_1: 8

 .= Z by XBOOLE_1: 28;

 for x1 st x1 in Z holds (( - ( sin | Z)) . x1) = ( diff (x,x1))

 proof

 let x1 such that

 A10: x1 in Z;

 reconsider x1 as Element of REAL by XREAL_0:def 1;



 A11: (( - ( sin | Z)) . x1) = ((( - sin ) | Z) . x1) by RFUNCT_1: 46

 .= (( - sin ) . x1) by A10, FUNCT_1: 49

 .= ( - ( sin . x1)) by RFUNCT_1: 58

 .= ( - (( sin | Z) . x1)) by A10, FUNCT_1: 49;

 ( diff (x,x1)) = ( - ( sin . x1)) by SIN_COS: 67

 .= (( - ( sin | Z)) . x1) by A11, A10, FUNCT_1: 49;

 hence thesis;

 end;

 then

 A12: (x `| Z) is continuous by A6, A8, A9, FDIFF_1:def 7;

 cos = ( cos | REAL );

 then

 A13: ( cos | Z) is continuous by FCONT_1: 16;



 A14: ( dom ( cos | Z)) = (( dom cos ) /\ Z) by RELAT_1: 61

 .= Z by SIN_COS: 24, XBOOLE_1: 28;

 for x1 st x1 in Z holds (( cos | Z) . x1) = ( diff (y,x1))

 proof

 let x1 such that

 A15: x1 in Z;

 ( diff (y,x1)) = ( cos . x1) by SIN_COS: 68

 .= (( cos | Z) . x1) by A15, FUNCT_1: 49;

 hence thesis;

 end;

 then (y `| Z) is continuous by A7, A13, A14, FDIFF_1:def 7;

 hence thesis by A1, A3, A4, A5, A6, A7, A12, SIN_COS: 24;

 end;

 end

 definition

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

 end



 Lm1: for a,b be Real, x,y be PartFunc of REAL , REAL , Z1,Z2 be Subset of REAL , f be 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 + ( (#) 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, x,y be PartFunc of REAL , REAL , Z1,Z2 be Subset of REAL , f be PartFunc of COMPLEX , COMPLEX ;

 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 + ( (#) y)) | [.a, b.])) c= ( dom f);

 then

 A2: x is_differentiable_on Z1 & y is_differentiable_on Z1 by FDIFF_1: 26;

 consider u01,v01 be 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)) * )) by Def2;

 consider u02,v02 be 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)) * )) 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 be object st x0 in ( dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB)) holds ((((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0) = ((((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0)

 proof

 let x0 be object such that

 A10: x0 in ( dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB));

 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 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 thesis by A2, A13, A14, FDIFF_1:def 7;

 end;

 hence thesis by A8, A9, FUNCT_1:def 11;

 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 be object st x0 in ( dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB)) holds ((((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0) = ((((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0)

 proof

 let x0 be object such that

 A24: x0 in ( dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB));

 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 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 thesis by A1, A3, A4, A29, A32, FDIFF_1:def 7;

 end;

 hence thesis by A22, A23, FUNCT_1:def 11;

 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 thesis by A3, A4, A18;

 end;



 Lm2: for a,b be Real, x1,y1,x2,y2 be PartFunc of REAL , REAL , Z be Subset of REAL , f be 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 + ( (#) y1)) | [.a, b.])) c= ( dom f) & x2 is_differentiable_on Z & y2 is_differentiable_on Z & ( rng ((x2 + ( (#) 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, x1,y1,x2,y2 be PartFunc of REAL , REAL , Z be Subset of REAL , f be PartFunc of COMPLEX , COMPLEX ;

 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 + ( (#) y1)) | [.a, b.])) c= ( dom f) & x2 is_differentiable_on Z & y2 is_differentiable_on Z & ( rng ((x2 + ( (#) y2)) | [.a, b.])) c= ( dom f);

 consider u01,v01 be 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)) * )) by Def2;

 consider u02,v02 be 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)) * )) by Def2;

 reconsider AB = [.a, b.] as non empty closed_interval Subset of REAL by A1, MEASURE5: 14;

 A4:

 now

 assume

 A5: not (a = b or a < b);

 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;

 end;

 per cases by A4;

 suppose

 A6: a < b;



 A7: (u01 | AB) = (u02 | AB)

 proof



 A8: ( dom (u01 | AB)) = ( dom (u02 | AB))

 proof



 A9: for x0 be object st x0 in ( dom (u01 | AB)) holds x0 in ( dom (u02 | AB))

 proof

 let x0 be object such that

 A10: x0 in ( dom (u01 | 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 thesis by RELAT_1: 61;

 end;

 for x0 be object st x0 in ( dom (u02 | AB)) holds x0 in ( dom (u01 | AB))

 proof

 let x0 be object such that

 A13: x0 in ( dom (u02 | 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 thesis by RELAT_1: 61;

 end;

 hence thesis by A9, TARSKI: 2;

 end;

 for x0 be object st x0 in ( dom (u01 | AB)) holds ((u01 | AB) . x0) = ((u02 | AB) . x0)

 proof

 let x0 be object such that

 A16: x0 in ( dom (u01 | AB));

 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 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 thesis by A17, A18, A19, A21, A22, A23, FUNCT_3: 48;

 end;

 hence thesis by A8, FUNCT_1:def 11;

 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 be object st x0 in ( dom ((x1 `| Z) | AB)) holds (((x1 `| Z) | AB) . x0) = (((x2 `| Z) | AB) . x0)

 proof

 let x0 be object such that

 A27: x0 in ( dom ((x1 `| Z) | AB));

 x0 in ( dom (x1 `| Z)) by A27, RELAT_1: 57;

 then

 reconsider 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

 assume

 A32: not (x0 in ].a, b.[ or x0 = a or x0 = b);

 x0 in { r where r be Real : a <= r & r <= b } by A25, A27, RCOMP_1:def 1;

 then

 A33: ex r be Real st r = x0 & a <= r & r <= b;

 A34:

 now

 assume

 A35: not (a = x0 or a < x0);

 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;

 end;

 A36:

 now

 assume

 A37: not (x0 = b or x0 < b);

 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;

 end;

 not (x0 in { q where q be Real : a < q & q < b }) by A32, RCOMP_1:def 2;

 hence contradiction by A32, A34, A36;

 end;

 ( diff (x1,x0)) = ( diff (x2,x0))

 proof

 per cases by A31;

 suppose

 A38: x0 = a;

 then x0 in { r where r be 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, c1 st ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (x1 - x2)) & (for n be Nat holds (h . n) > 0 ) holds ( lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)))) = 0

 proof

 let h, c1 such that

 A45: ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (x1 - x2)) & (for n be Nat holds (h . n) > 0 );



 A46: h is convergent & ( lim h) = 0 ;



 A47: 0 < (b - x0) by A6, A38, XREAL_1: 50;

 then

 consider n be Nat such that

 A48: for m be Nat st n <= m holds |.((h . m) - 0 ).| < ((b - x0) / 2) by A46, SEQ_2:def 7;



 A49: for p1 st 0 < p1 holds ex n1 be Nat st for m be Nat st n1 <= m holds |.((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ).| < p1

 proof

 let p1 such that

 A50: 0 < p1;

 take n;

 for m be Nat st n <= m holds (((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) = 0

 proof

 let m be Nat such that

 A51: n <= m;



 A52: m in NAT by ORDINAL1:def 12;



 A53: |.((h . m) - 0 ).| < ((b - x0) / 2) by A48, A51;



 A54: 0 < (h . m) by A45;

 then

 A55: (h . m) < ((b - x0) / 2) by A53, ABSVALUE:def 1;



 A56: (a + 0 ) <= (x0 + (h . m)) by A38, A54, XREAL_1: 7;

 (x0 + (h . m)) <= (x0 + ((b - x0) / 2)) by A55, XREAL_1: 7;

 then

 A57: ((x0 + (h . m)) + 0 ) <= ((b - ((b - x0) / 2)) + ((b - x0) / 2)) by A47, XREAL_1: 7;



 A58: [.a, b.] c= (( dom x1) /\ ( dom x2)) by A1, XBOOLE_1: 19;

 then x0 in (( dom x1) /\ ( dom x2)) by A39;

 then

 A59: x0 in ( dom (x1 - x2)) by VALUED_1: 12;



 A60: [.a, b.] c= ( dom (x1 - x2)) by A58, VALUED_1: 12;

 (x0 + (h . m)) in { r where r be Real : a <= r & r <= b } by A56, A57;

 then

 A61: (x0 + (h . m)) in [.a, b.] by RCOMP_1:def 1;



 A62: x0 in ( rng c1) by A45, TARSKI:def 1;



 A63: ( lim c1) = (c1 . m) by SEQ_4: 26;



 A64: ((h + c1) . m) = ((h . m) + (c1 . m)) by SEQ_1: 7

 .= ((h . m) + x0) by A62, A63, SEQ_4: 25;



 A65: ( rng c1) c= ( dom (x1 - x2)) by A45, A59, TARSKI:def 1;



 A66: (((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, A52

 .= (((h " ) . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m)))) by A65, FUNCT_2: 108, A52

 .= (((h " ) . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0))) by A62, A63, A64, SEQ_4: 25;



 A67: ((x1 - x2) . ((h . m) + x0)) = ((x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0))) by A60, A61, VALUED_1: 13

 .= (((x1 | [.a, b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0))) by A61, FUNCT_1: 49

 .= (((x1 | [.a, b.]) . ((h . m) + x0)) - ((x2 | [.a, b.]) . ((h . m) + x0))) by A61, FUNCT_1: 49

 .= 0 by A1;

 ((x1 - x2) . x0) = ((x1 . x0) - (x2 . x0)) by A59, 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 thesis by A66, A67;

 end;

 hence thesis by A50, COMPLEX1: 44;

 end;

 then ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) is convergent by SEQ_2:def 6;

 hence thesis by A49, SEQ_2:def 7;

 end;

 then (( Rdiff (x1,x0)) - ( Rdiff (x2,x0))) = 0 by A43, A44, FDIFF_3:def 6;

 hence thesis;

 end;

 hence thesis by A40, A42, FDIFF_3: 22;

 end;

 suppose

 A68: x0 in ].a, b.[;



 A69: ].a, b.[ is open by RCOMP_1: 7;



 A70: ].a, b.[ c= [.a, b.]

 proof

 for x0 be object st x0 in ].a, b.[ holds x0 in [.a, b.]

 proof

 let x0 be object such that

 A71: x0 in ].a, b.[;

 x0 in { r where r be Real : a < r & r < b } by A71, RCOMP_1:def 2;

 then

 A72: ex r st r = x0 & a < r & r < b;

 then

 reconsider x0 as Real;

 x0 in { r where r be Real : a <= r & r <= b } by A72;

 hence thesis by RCOMP_1:def 1;

 end;

 hence thesis;

 end;

 then

 A73: x1 is_differentiable_on ].a, b.[ by A1, A69, FDIFF_1: 26, XBOOLE_1: 1;

 then

 A74: (x1 | ].a, b.[) is_differentiable_on ].a, b.[ & ((x1 | ].a, b.[) `| ].a, b.[) = (x1 `| ].a, b.[) by A69, FDIFF_2: 16;



 A75: ((x1 `| ].a, b.[) . x0) = ( diff (x1,x0)) by A68, A73, FDIFF_1:def 7;



 A76: x2 is_differentiable_on ].a, b.[ by A69, A70, A1, FDIFF_1: 26, XBOOLE_1: 1;

 then

 A77: (x2 | ].a, b.[) is_differentiable_on ].a, b.[ & ((x2 | ].a, b.[) `| ].a, b.[) = (x2 `| ].a, b.[) by A69, FDIFF_2: 16;



 A78: ((x2 `| ].a, b.[) . x0) = ( diff (x2,x0)) by A68, A76, FDIFF_1:def 7;



 A79: ( dom (x1 | ].a, b.[)) = (( dom x1) /\ ].a, b.[) by RELAT_1: 61

 .= ].a, b.[ by A1, A70, XBOOLE_1: 1, XBOOLE_1: 28

 .= (( dom x2) /\ ].a, b.[) by A1, A70, XBOOLE_1: 1, XBOOLE_1: 28

 .= ( dom (x2 | ].a, b.[)) by RELAT_1: 61;

 for x0 be object st x0 in ( dom (x1 | ].a, b.[)) holds ((x1 | ].a, b.[) . x0) = ((x2 | ].a, b.[) . x0)

 proof

 let x0 be object such that

 A80: x0 in ( dom (x1 | ].a, b.[));



 A81: ( dom (x1 | ].a, b.[)) = (( dom x1) /\ ].a, b.[) by RELAT_1: 61

 .= ].a, b.[ by A1, A70, XBOOLE_1: 1, XBOOLE_1: 28;



 then ((x1 | ].a, b.[) . x0) = (x1 . x0) by A80, FUNCT_1: 49

 .= ((x1 | [.a, b.]) . x0) by A70, A80, A81, FUNCT_1: 49

 .= (x2 . x0) by A70, A80, A81, A1, FUNCT_1: 49

 .= ((x2 | ].a, b.[) . x0) by A80, A81, FUNCT_1: 49;

 hence thesis;

 end;

 hence thesis by A74, A75, A77, A78, A79, FUNCT_1: 2;

 end;

 suppose

 A82: x0 = b;

 then x0 in { r where r be Real : a <= r & r <= b } by A1;

 then

 A83: x0 in [.a, b.] by RCOMP_1:def 1;

 then

 A84: x1 is_differentiable_in x0 by A1, FDIFF_1: 9;

 then

 A85: x1 is_left_differentiable_in x0 & ( diff (x1,x0)) = ( Ldiff (x1,x0)) by FDIFF_3: 22;

 x2 is_differentiable_in x0 by A1, A83, FDIFF_1: 9;

 then

 A86: x2 is_left_differentiable_in x0 & ( diff (x2,x0)) = ( Ldiff (x2,x0)) by FDIFF_3: 22;

 then

 A87: (x1 - x2) is_left_differentiable_in x0 by A85, FDIFF_3: 11;

 ( Ldiff (x1,x0)) = ( Ldiff (x2,x0))

 proof



 A88: (( Ldiff (x1,x0)) - ( Ldiff (x2,x0))) = ( Ldiff ((x1 - x2),x0)) by A85, A86, FDIFF_3: 11;

 for h, c1 st ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (x1 - x2)) & (for n be Nat holds (h . n) < 0 ) holds ( lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)))) = 0

 proof

 let h, c1 such that

 A89: ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (x1 - x2)) & (for n be Nat holds (h . n) < 0 );



 A90: h is convergent & ( lim h) = 0 ;



 A91: 0 < (b - a) by A6, XREAL_1: 50;

 then

 consider n be Nat such that

 A92: for m be Nat st n <= m holds |.((h . m) - 0 ).| < ((x0 - a) / 2) by A82, A90, SEQ_2:def 7;



 A93: for p1 st 0 < p1 holds ex n1 be Nat st for m be Nat st n1 <= m holds |.((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ).| < p1

 proof

 let p1 such that

 A94: 0 < p1;

 take n;

 for m be Nat st n <= m holds (((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) = 0

 proof

 let m be Nat such that

 A95: n <= m;



 A96: m in NAT by ORDINAL1:def 12;



 A97: |.((h . m) - 0 ).| < ((x0 - a) / 2) by A92, A95;



 A98: (h . m) < 0 by A89;

 then

 A99: ( - (h . m)) < ((x0 - a) / 2) by A97, ABSVALUE:def 1;



 A100: (x0 + (h . m)) <= (b + 0 ) by A82, A98, XREAL_1: 7;

 (x0 - ((x0 - a) / 2)) <= (x0 - ( - (h . m))) by A99, XREAL_1: 13;

 then

 A101: ((a + ((x0 - a) / 2)) - ((x0 - a) / 2)) <= ((x0 + (h . m)) - 0 ) by A82, A91, XREAL_1: 13;



 A102: [.a, b.] c= (( dom x1) /\ ( dom x2)) by A1, XBOOLE_1: 19;

 then x0 in (( dom x1) /\ ( dom x2)) by A83;

 then

 A103: x0 in ( dom (x1 - x2)) by VALUED_1: 12;



 A104: [.a, b.] c= ( dom (x1 - x2)) by A102, VALUED_1: 12;

 (x0 + (h . m)) in { r where r be Real : a <= r & r <= b } by A100, A101;

 then

 A105: (x0 + (h . m)) in [.a, b.] by RCOMP_1:def 1;

 x0 in ( rng c1) by A89, TARSKI:def 1;

 then

 A106: ( lim c1) = x0 by SEQ_4: 25;



 A107: ((h + c1) . m) = ((h . m) + (c1 . m)) by SEQ_1: 7

 .= ((h . m) + x0) by A106, SEQ_4: 26;



 A108: ( rng c1) c= ( dom (x1 - x2)) by A89, A103, TARSKI:def 1;



 A109: (((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 A89, FUNCT_2: 108, A96

 .= (((h " ) . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m)))) by A108, FUNCT_2: 108, A96

 .= (((h " ) . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0))) by A106, A107, SEQ_4: 26;



 A110: ((x1 - x2) . ((h . m) + x0)) = ((x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0))) by A104, A105, VALUED_1: 13

 .= (((x1 | [.a, b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0))) by A105, FUNCT_1: 49

 .= (((x1 | [.a, b.]) . ((h . m) + x0)) - ((x2 | [.a, b.]) . ((h . m) + x0))) by A105, FUNCT_1: 49

 .= 0 by A1;

 ((x1 - x2) . x0) = ((x1 . x0) - (x2 . x0)) by A103, VALUED_1: 13

 .= (((x1 | [.a, b.]) . x0) - (x2 . x0)) by A83, FUNCT_1: 49

 .= (((x1 | [.a, b.]) . x0) - ((x2 | [.a, b.]) . x0)) by A83, FUNCT_1: 49

 .= 0 by A1;

 hence thesis by A109, A110;

 end;

 hence thesis by A94, COMPLEX1: 44;

 end;

 then ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) is convergent by SEQ_2:def 6;

 hence thesis by A93, SEQ_2:def 7;

 end;

 then ( Ldiff ((x1 - x2),x0)) = 0 by A87, FDIFF_3:def 5;

 hence thesis by A88;

 end;

 hence thesis by A84, A86, FDIFF_3: 22;

 end;

 end;

 hence thesis by A27, A28, A29, A30, FUNCT_1: 49;

 end;

 hence thesis by A25, A26, FUNCT_1:def 11;

 end;



 A111: (v01 | AB) = (v02 | AB)

 proof



 A112: ( dom (v01 | AB)) = ( dom (v02 | AB))

 proof



 A113: for x0 be object st x0 in ( dom (v01 | AB)) holds x0 in ( dom (v02 | AB))

 proof

 let x0 be object such that

 A114: x0 in ( dom (v01 | AB));

 x0 in (( dom v01) /\ AB) by A114, RELAT_1: 61;

 then

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

 A116: 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, A115, 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 A116, 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 thesis by RELAT_1: 61;

 end;

 for x0 be object st x0 in ( dom (v02 | AB)) holds x0 in ( dom (v01 | AB))

 proof

 let x0 be object such that

 A117: x0 in ( dom (v02 | AB));

 x0 in (( dom v02) /\ AB) by A117, RELAT_1: 61;

 then

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

 A119: 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, A118, 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 A119, 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 thesis by RELAT_1: 61;

 end;

 hence thesis by A113, TARSKI: 2;

 end;

 for x0 be object st x0 in ( dom (v01 | AB)) holds ((v01 | AB) . x0) = ((v02 | AB) . x0)

 proof

 let x0 be object such that

 A120: x0 in ( dom (v01 | AB));

 x0 in (( dom v01) /\ AB) by A120, RELAT_1: 61;

 then

 A121: x0 in AB & x0 in ( dom v01) by XBOOLE_0:def 4;

 then

 reconsider x0 as Real;



 A122: AB c= (( dom x1) /\ ( dom y1)) by A1, XBOOLE_1: 19;

 then x0 in (( dom x1) /\ ( dom y1)) by A121;

 then x0 in ( dom <:x1, y1:>) by FUNCT_3:def 7;

 then

 A123: (v01 . x0) = ((( Im f) * R2-to-C ) . ( <:x1, y1:> . x0)) by A2, FUNCT_1: 13;



 A124: AB c= (( dom x2) /\ ( dom y2)) by A1, XBOOLE_1: 19;

 then x0 in (( dom x2) /\ ( dom y2)) by A121;

 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

 A125: (v02 . x0) = ((( Im f) * R2-to-C ) . [(x2 . x0), (y2 . x0)]) by A121, A124, FUNCT_3: 48;



 A126: (x1 . x0) = ((x1 | [.a, b.]) . x0) by A121, FUNCT_1: 49

 .= (x2 . x0) by A121, A1, FUNCT_1: 49;



 A127: (y1 . x0) = ((y1 | [.a, b.]) . x0) by A121, FUNCT_1: 49

 .= (y2 . x0) by A121, A1, FUNCT_1: 49;

 (v01 . x0) = ((v01 | AB) . x0) & (v02 . x0) = ((v02 | AB) . x0) by A121, FUNCT_1: 49;

 hence thesis by A126, A127, A123, A121, A122, A125, FUNCT_3: 48;

 end;

 hence thesis by A112, FUNCT_1:def 11;

 end;



 A128: ((y1 `| Z) | AB) = ((y2 `| Z) | AB)

 proof



 A129: ( 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;



 A130: ( 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 be object st x0 in ( dom ((y1 `| Z) | AB)) holds (((y1 `| Z) | AB) . x0) = (((y2 `| Z) | AB) . x0)

 proof

 let x0 be object such that

 A131: x0 in ( dom ((y1 `| Z) | AB));

 x0 in ( dom (y1 `| Z)) by A131, RELAT_1: 57;

 then

 reconsider x0 as Real;



 A132: (((y2 `| Z) | AB) . x0) = ((y2 `| Z) . x0) by A131, FUNCT_1: 49;



 A133: ((y1 `| Z) . x0) = ( diff (y1,x0)) by A1, A131, A129, FDIFF_1:def 7;



 A134: ((y2 `| Z) . x0) = ( diff (y2,x0)) by A1, A131, A129, FDIFF_1:def 7;

 A135:

 now

 assume

 A136: not (x0 in ].a, b.[ or x0 = a or x0 = b);

 x0 in { r where r be Real : a <= r & r <= b } by A129, A131, RCOMP_1:def 1;

 then

 A137: ex r be Real st r = x0 & a <= r & r <= b;

 A138:

 now

 assume

 A139: not (a = x0 or a < x0);

 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 A137, A139;

 end;

 A140:

 now

 assume

 A141: not (x0 = b or x0 < b);

 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 A137, A141;

 end;

 not (x0 in { q where q be Real : a < q & q < b }) by A136, RCOMP_1:def 2;

 hence contradiction by A136, A138, A140;

 end;

 ( diff (y1,x0)) = ( diff (y2,x0))

 proof

 per cases by A135;

 suppose

 A142: x0 = a;

 then x0 in { r where r be Real : a <= r & r <= b } by A1;

 then

 A143: x0 in [.a, b.] by RCOMP_1:def 1;

 then

 A144: y1 is_differentiable_in x0 by A1, FDIFF_1: 9;

 then

 A145: y1 is_right_differentiable_in x0 & ( diff (y1,x0)) = ( Rdiff (y1,x0)) by FDIFF_3: 22;

 y2 is_differentiable_in x0 by A1, A143, FDIFF_1: 9;

 then

 A146: y2 is_right_differentiable_in x0 & ( diff (y2,x0)) = ( Rdiff (y2,x0)) by FDIFF_3: 22;

 then

 A147: (y1 - y2) is_right_differentiable_in x0 by A145, FDIFF_3: 17;

 ( Rdiff (y1,x0)) = ( Rdiff (y2,x0))

 proof



 A148: (( Rdiff (y1,x0)) - ( Rdiff (y2,x0))) = ( Rdiff ((y1 - y2),x0)) by A145, A146, FDIFF_3: 17;

 for h, c1 st ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (y1 - y2)) & (for n be Nat holds (h . n) > 0 ) holds ( lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)))) = 0

 proof

 let h, c1 such that

 A149: ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (y1 - y2)) & (for n be Nat holds (h . n) > 0 );



 A150: h is convergent & ( lim h) = 0 ;



 A151: 0 < (b - x0) by A6, A142, XREAL_1: 50;

 then

 consider n be Nat such that

 A152: for m be Nat st n <= m holds |.((h . m) - 0 ).| < ((b - x0) / 2) by A150, SEQ_2:def 7;



 A153: for p1 st 0 < p1 holds ex n1 be Nat st for m be Nat st n1 <= m holds |.((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ).| < p1

 proof

 let p1 such that

 A154: 0 < p1;

 take n;

 for m be Nat st n <= m holds (((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) = 0

 proof

 let m be Nat such that

 A155: n <= m;



 A156: |.((h . m) - 0 ).| < ((b - x0) / 2) by A152, A155;



 A157: m in NAT by ORDINAL1:def 12;



 A158: 0 < (h . m) by A149;

 then

 A159: (h . m) < ((b - x0) / 2) by A156, ABSVALUE:def 1;



 A160: (a + 0 ) <= (x0 + (h . m)) by A142, A158, XREAL_1: 7;

 (x0 + (h . m)) <= (x0 + ((b - x0) / 2)) by A159, XREAL_1: 7;

 then

 A161: ((x0 + (h . m)) + 0 ) <= ((b - ((b - x0) / 2)) + ((b - x0) / 2)) by A151, XREAL_1: 7;



 A162: [.a, b.] c= (( dom y1) /\ ( dom y2)) by A1, XBOOLE_1: 19;

 then x0 in (( dom y1) /\ ( dom y2)) by A143;

 then

 A163: x0 in ( dom (y1 - y2)) by VALUED_1: 12;



 A164: [.a, b.] c= ( dom (y1 - y2)) by A162, VALUED_1: 12;

 (x0 + (h . m)) in { r where r be Real : a <= r & r <= b } by A160, A161;

 then

 A165: (x0 + (h . m)) in [.a, b.] by RCOMP_1:def 1;



 A166: x0 in ( rng c1) by A149, TARSKI:def 1;



 A167: ( lim c1) = (c1 . m) by SEQ_4: 26;



 A168: ((h + c1) . m) = ((h . m) + (c1 . m)) by SEQ_1: 7

 .= ((h . m) + x0) by A167, A166, SEQ_4: 25;



 A169: ( rng c1) c= ( dom (y1 - y2)) by A163, A149, TARSKI:def 1;



 A170: (((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 A149, FUNCT_2: 108, A157

 .= (((h " ) . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m)))) by A169, FUNCT_2: 108, A157

 .= (((h " ) . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0))) by A166, A167, A168, SEQ_4: 25;



 A171: ((y1 - y2) . ((h . m) + x0)) = ((y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0))) by A164, A165, VALUED_1: 13

 .= (((y1 | [.a, b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0))) by A165, FUNCT_1: 49

 .= (((y1 | [.a, b.]) . ((h . m) + x0)) - ((y2 | [.a, b.]) . ((h . m) + x0))) by A165, FUNCT_1: 49

 .= 0 by A1;

 ((y1 - y2) . x0) = ((y1 . x0) - (y2 . x0)) by A163, VALUED_1: 13

 .= (((y1 | [.a, b.]) . x0) - (y2 . x0)) by A143, FUNCT_1: 49

 .= (((y1 | [.a, b.]) . x0) - ((y2 | [.a, b.]) . x0)) by A143, FUNCT_1: 49

 .= 0 by A1;

 hence thesis by A170, A171;

 end;

 hence thesis by A154, COMPLEX1: 44;

 end;

 then ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) is convergent by SEQ_2:def 6;

 hence thesis by A153, SEQ_2:def 7;

 end;

 then (( Rdiff (y1,x0)) - ( Rdiff (y2,x0))) = 0 by A147, A148, FDIFF_3:def 6;

 hence thesis;

 end;

 hence thesis by A144, A146, FDIFF_3: 22;

 end;

 suppose

 A172: x0 in ].a, b.[;



 A173: ].a, b.[ is open by RCOMP_1: 7;



 A174: ].a, b.[ c= [.a, b.]

 proof

 for x0 be object st x0 in ].a, b.[ holds x0 in [.a, b.]

 proof

 let x0 be object such that

 A175: x0 in ].a, b.[;

 x0 in { r where r be Real : a < r & r < b } by A175, RCOMP_1:def 2;

 then

 A176: ex r st r = x0 & a < r & r < b;

 then

 reconsider x0 as Real;

 x0 in { r where r be Real : a <= r & r <= b } by A176;

 hence thesis by RCOMP_1:def 1;

 end;

 hence thesis;

 end;

 then

 A177: y1 is_differentiable_on ].a, b.[ by A1, A173, FDIFF_1: 26, XBOOLE_1: 1;

 then

 A178: (y1 | ].a, b.[) is_differentiable_on ].a, b.[ & ((y1 | ].a, b.[) `| ].a, b.[) = (y1 `| ].a, b.[) by A173, FDIFF_2: 16;



 A179: ((y1 `| ].a, b.[) . x0) = ( diff (y1,x0)) by A172, A177, FDIFF_1:def 7;



 A180: y2 is_differentiable_on ].a, b.[ by A1, A173, A174, FDIFF_1: 26, XBOOLE_1: 1;

 then

 A181: (y2 | ].a, b.[) is_differentiable_on ].a, b.[ & ((y2 | ].a, b.[) `| ].a, b.[) = (y2 `| ].a, b.[) by A173, FDIFF_2: 16;



 A182: ((y2 `| ].a, b.[) . x0) = ( diff (y2,x0)) by A172, A180, FDIFF_1:def 7;



 A183: ( dom (y1 | ].a, b.[)) = (( dom y1) /\ ].a, b.[) by RELAT_1: 61

 .= ].a, b.[ by A1, A174, XBOOLE_1: 1, XBOOLE_1: 28

 .= (( dom y2) /\ ].a, b.[) by A1, A174, XBOOLE_1: 1, XBOOLE_1: 28

 .= ( dom (y2 | ].a, b.[)) by RELAT_1: 61;

 for x0 be object st x0 in ( dom (y1 | ].a, b.[)) holds ((y1 | ].a, b.[) . x0) = ((y2 | ].a, b.[) . x0)

 proof

 let x0 be object such that

 A184: x0 in ( dom (y1 | ].a, b.[));



 A185: ( dom (y1 | ].a, b.[)) = (( dom y1) /\ ].a, b.[) by RELAT_1: 61

 .= ].a, b.[ by A1, A174, XBOOLE_1: 1, XBOOLE_1: 28;



 then ((y1 | ].a, b.[) . x0) = (y1 . x0) by A184, FUNCT_1: 49

 .= ((y1 | [.a, b.]) . x0) by A174, A184, A185, FUNCT_1: 49

 .= (y2 . x0) by A174, A184, A185, A1, FUNCT_1: 49

 .= ((y2 | ].a, b.[) . x0) by A184, A185, FUNCT_1: 49;

 hence thesis;

 end;

 hence thesis by A178, A179, A181, A182, A183, FUNCT_1: 2;

 end;

 suppose

 A186: x0 = b;

 then x0 in { r where r be Real : a <= r & r <= b } by A1;

 then

 A187: x0 in [.a, b.] by RCOMP_1:def 1;

 then

 A188: y1 is_differentiable_in x0 by A1, FDIFF_1: 9;

 then

 A189: y1 is_left_differentiable_in x0 & ( diff (y1,x0)) = ( Ldiff (y1,x0)) by FDIFF_3: 22;

 y2 is_differentiable_in x0 by A1, A187, FDIFF_1: 9;

 then

 A190: y2 is_left_differentiable_in x0 & ( diff (y2,x0)) = ( Ldiff (y2,x0)) by FDIFF_3: 22;

 then

 A191: (y1 - y2) is_left_differentiable_in x0 by A189, FDIFF_3: 11;

 ( Ldiff (y1,x0)) = ( Ldiff (y2,x0))

 proof



 A192: (( Ldiff (y1,x0)) - ( Ldiff (y2,x0))) = ( Ldiff ((y1 - y2),x0)) by A189, A190, FDIFF_3: 11;

 for h, c1 st ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (y1 - y2)) & (for n be Nat holds (h . n) < 0 ) holds ( lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)))) = 0

 proof

 let h, c1 such that

 A193: ( rng c1) = {x0} & ( rng (h + c1)) c= ( dom (y1 - y2)) & (for n be Nat holds (h . n) < 0 );



 A194: h is convergent & ( lim h) = 0 ;



 A195: 0 < (b - a) by A6, XREAL_1: 50;

 then

 consider n be Nat such that

 A196: for m be Nat st n <= m holds |.((h . m) - 0 ).| < ((x0 - a) / 2) by A186, A194, SEQ_2:def 7;



 A197: for p1 st 0 < p1 holds ex n1 be Nat st for m be Nat st n1 <= m holds |.((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ).| < p1

 proof

 let p1 such that

 A198: 0 < p1;

 take n;

 for m be Nat st n <= m holds (((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) = 0

 proof

 let m be Nat such that

 A199: n <= m;



 A200: |.((h . m) - 0 ).| < ((x0 - a) / 2) by A196, A199;



 A201: m in NAT by ORDINAL1:def 12;



 A202: (h . m) < 0 by A193;

 then

 A203: ( - (h . m)) < ((x0 - a) / 2) by A200, ABSVALUE:def 1;



 A204: (x0 + (h . m)) <= (b + 0 ) by A186, A202, XREAL_1: 7;

 (x0 - ((x0 - a) / 2)) <= (x0 - ( - (h . m))) by A203, XREAL_1: 13;

 then

 A205: ((a + ((x0 - a) / 2)) - ((x0 - a) / 2)) <= ((x0 + (h . m)) - 0 ) by A186, A195, XREAL_1: 13;



 A206: [.a, b.] c= (( dom y1) /\ ( dom y2)) by A1, XBOOLE_1: 19;

 then x0 in (( dom y1) /\ ( dom y2)) by A187;

 then

 A207: x0 in ( dom (y1 - y2)) by VALUED_1: 12;



 A208: [.a, b.] c= ( dom (y1 - y2)) by A206, VALUED_1: 12;

 (x0 + (h . m)) in { r where r be Real : a <= r & r <= b } by A204, A205;

 then

 A209: (x0 + (h . m)) in [.a, b.] by RCOMP_1:def 1;

 x0 in ( rng c1) by A193, TARSKI:def 1;

 then

 A210: ( lim c1) = x0 by SEQ_4: 25;



 A211: ((h + c1) . m) = ((h . m) + (c1 . m)) by SEQ_1: 7

 .= ((h . m) + x0) by A210, SEQ_4: 26;



 A212: ( rng c1) c= ( dom (y1 - y2)) by A193, A207, TARSKI:def 1;



 A213: (((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 A193, FUNCT_2: 108, A201

 .= (((h " ) . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m)))) by A212, FUNCT_2: 108, A201

 .= (((h " ) . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0))) by A210, A211, SEQ_4: 26;



 A214: ((y1 - y2) . ((h . m) + x0)) = ((y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0))) by A208, A209, VALUED_1: 13

 .= (((y1 | [.a, b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0))) by A209, FUNCT_1: 49

 .= (((y1 | [.a, b.]) . ((h . m) + x0)) - ((y2 | [.a, b.]) . ((h . m) + x0))) by A209, FUNCT_1: 49

 .= 0 by A1;

 ((y1 - y2) . x0) = ((y1 . x0) - (y2 . x0)) by A207, VALUED_1: 13

 .= (((y1 | [.a, b.]) . x0) - (y2 . x0)) by A187, FUNCT_1: 49

 .= (((y1 | [.a, b.]) . x0) - ((y2 | [.a, b.]) . x0)) by A187, FUNCT_1: 49

 .= 0 by A1;

 hence thesis by A213, A214;

 end;

 hence thesis by A198, COMPLEX1: 44;

 end;

 then ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) is convergent by SEQ_2:def 6;

 hence thesis by A197, SEQ_2:def 7;

 end;

 then ( Ldiff ((y1 - y2),x0)) = 0 by A191, FDIFF_3:def 5;

 hence thesis by A192;

 end;

 hence thesis by A188, A190, FDIFF_3: 22;

 end;

 end;

 hence thesis by A131, A132, A133, A134, FUNCT_1: 49;

 end;

 hence thesis by A129, A130, FUNCT_1:def 11;

 end;



 A215: (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB) = (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB)

 proof



 A216: (x1 `| Z) is PartFunc of REAL , COMPLEX & (y1 `| Z) is PartFunc of REAL , COMPLEX by NUMBERS: 11, RELSET_1: 7;



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

 A218: (((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 A216, A217, CFUNCT_1: 53

 .= (((u01 | AB) (#) ((x1 `| Z) | AB)) - ((v01 | AB) (#) ((y1 `| Z) | AB))) by A216, A217, CFUNCT_1: 53;



 A219: (x2 `| Z) is PartFunc of REAL , COMPLEX & (y2 `| Z) is PartFunc of REAL , COMPLEX by NUMBERS: 11, RELSET_1: 7;



 A220: 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 A219, A220, CFUNCT_1: 53

 .= (((u02 | AB) (#) ((x2 `| Z) | AB)) - ((v02 | AB) (#) ((y2 `| Z) | AB))) by A219, A220, CFUNCT_1: 53;

 hence thesis by A7, A24, A111, A128, A218;

 end;



 A221: ( 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 A215

 .= ( integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b)) by INTEGRA5: 19;



 A222: (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB) = (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB)

 proof



 A223: (x1 `| Z) is PartFunc of REAL , COMPLEX & (y1 `| Z) is PartFunc of REAL , COMPLEX by NUMBERS: 11, RELSET_1: 7;



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

 A225: (((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 A223, A224, CFUNCT_1: 53

 .= (((v01 | AB) (#) ((x1 `| Z) | AB)) + ((u01 | AB) (#) ((y1 `| Z) | AB))) by A223, A224, CFUNCT_1: 53;



 A226: (x2 `| Z) is PartFunc of REAL , COMPLEX & (y2 `| Z) is PartFunc of REAL , COMPLEX by NUMBERS: 11, RELSET_1: 7;



 A227: 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 A226, A227, CFUNCT_1: 53

 .= (((v02 | AB) (#) ((x2 `| Z) | AB)) + ((u02 | AB) (#) ((y2 `| Z) | AB))) by A226, A227, CFUNCT_1: 53;

 hence thesis by A7, A24, A111, A128, A225;

 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 A222

 .= ( integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b)) by INTEGRA5: 19;

 hence thesis by A2, A3, A221;

 end;

 suppose

 A228: a = b;

 then

 reconsider BA = [.b, a.] as non empty closed_interval Subset of REAL by MEASURE5: 14;



 A229: ( integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b)) = ( integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),BA)) by A228, INTEGRA5: 19;



 A230: ( - ( integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),BA))) = ( integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b)) by INTEGRA5: 20;



 A231: ( integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b)) = ( integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),BA)) by A228, INTEGRA5: 19;



 A232: ( - ( 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 A228, INTEGRA5: 19;

 then

 A233: ( 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 A228, INTEGRA5: 20;

 hence thesis by A2, A3, A229, A230, A231, A232, A233;

 end;

 end;

 definition

 let f be PartFunc of COMPLEX , COMPLEX ;

 let C be C1-curve;

 assume

 A1: ( rng C) c= ( dom f);

 :: INTEGR1C:def4

 func integral (f,C) -> Complex means

 : Def4: ex a,b be Real, x,y be PartFunc of REAL , REAL , Z be 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 + ( (#) y)) | [.a, b.]) & it = ( integral (f,x,y,a,b,Z));

 existence

 proof

 consider a,b be Real, x,y be PartFunc of REAL , REAL , Z be 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 + ( (#) y)) | [.a, b.]) by Def3;

 reconsider a, b as Real;

 take ( integral (f,x,y,a,b,Z));

 thus thesis by A2;

 end;

 uniqueness

 proof

 let s1,s2 be Complex;

 assume

 A3: ex a,b be Real, x,y be PartFunc of REAL , REAL , Z be 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 + ( (#) y)) | [.a, b.]) & s1 = ( integral (f,x,y,a,b,Z));

 assume

 A4: ex a,b be Real, x,y be PartFunc of REAL , REAL , Z be 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 + ( (#) y)) | [.a, b.]) & s2 = ( integral (f,x,y,a,b,Z));

 consider a1,b1 be Real, x1,y1 be PartFunc of REAL , REAL , Z1 be 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 + ( (#) y1)) | [.a1, b1.]) & s1 = ( integral (f,x1,y1,a1,b1,Z1)) by A3;

 consider a2,b2 be Real, x2,y2 be PartFunc of REAL , REAL , Z2 be 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 + ( (#) 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 be set st x0 in [.a1, b1.] holds (x1 . x0) = (x2 . x0)

 proof

 let x0 be set such that

 A10: x0 in [.a1, b1.];



 A11: ( dom ( (#) y1)) = ( dom y1) by VALUED_1:def 5;

 ( dom (x1 + ( (#) y1))) = (( dom x1) /\ ( dom ( (#) y1))) by VALUED_1:def 1;

 then

 A12: [.a1, b1.] c= ( dom (x1 + ( (#) y1))) by A5, A11, XBOOLE_1: 19;



 A13: (((x1 + ( (#) y1)) | [.a1, b1.]) . x0) = ((x1 + ( (#) y1)) . x0) by A10, FUNCT_1: 49

 .= ((x1 . x0) + (( (#) y1) . x0)) by A10, A12, VALUED_1:def 1

 .= ((x1 . x0) + ( * (y1 . x0))) by VALUED_1: 6;



 A14: ( dom ( (#) y2)) = ( dom y2) by VALUED_1:def 5;

 ( dom (x2 + ( (#) y2))) = (( dom x2) /\ ( dom ( (#) y2))) by VALUED_1:def 1;

 then

 A15: [.a2, b2.] c= ( dom (x2 + ( (#) y2))) by A6, A14, XBOOLE_1: 19;

 (((x2 + ( (#) y2)) | [.a2, b2.]) . x0) = ((x2 + ( (#) y2)) . x0) by A6, A5, A10, FUNCT_1: 49

 .= ((x2 . x0) + (( (#) y2) . x0)) by A6, A5, A10, A15, VALUED_1:def 1

 .= ((x2 . x0) + ( * (y2 . x0))) by VALUED_1: 6;

 hence thesis by A6, A5, A13, COMPLEX1: 77;

 end;

 hence thesis by A5, A6, FUNCT_1: 95;

 end;



 A16: (y1 | [.a1, b1.]) = (y2 | [.a2, b2.])

 proof

 for x0 be set st x0 in [.a1, b1.] holds (y1 . x0) = (y2 . x0)

 proof

 let x0 be set such that

 A17: x0 in [.a1, b1.];



 A18: ( dom ( (#) y1)) = ( dom y1) by VALUED_1:def 5;

 ( dom (x1 + ( (#) y1))) = (( dom x1) /\ ( dom ( (#) y1))) by VALUED_1:def 1;

 then

 A19: [.a1, b1.] c= ( dom (x1 + ( (#) y1))) by A5, A18, XBOOLE_1: 19;



 A20: (((x1 + ( (#) y1)) | [.a1, b1.]) . x0) = ((x1 + ( (#) y1)) . x0) by A17, FUNCT_1: 49

 .= ((x1 . x0) + (( (#) y1) . x0)) by A17, A19, VALUED_1:def 1

 .= ((x1 . x0) + ( * (y1 . x0))) by VALUED_1: 6;



 A21: ( dom ( (#) y2)) = ( dom y2) by VALUED_1:def 5;

 ( dom (x2 + ( (#) y2))) = (( dom x2) /\ ( dom ( (#) y2))) by VALUED_1:def 1;

 then

 A22: [.a2, b2.] c= ( dom (x2 + ( (#) y2))) by A6, A21, XBOOLE_1: 19;

 (((x2 + ( (#) y2)) | [.a2, b2.]) . x0) = ((x2 + ( (#) y2)) . x0) by A5, A6, A17, FUNCT_1: 49

 .= ((x2 . x0) + (( (#) y2) . x0)) by A5, A6, A17, A22, VALUED_1:def 1

 .= ((x2 . x0) + ( * (y2 . x0))) by VALUED_1: 6;

 hence thesis by A6, A5, A20, COMPLEX1: 77;

 end;

 hence thesis by A5, A6, FUNCT_1: 95;

 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;

 end;

 end

 definition

 let f be PartFunc of COMPLEX , COMPLEX ;

 let C be C1-curve;

 :: INTEGR1C:def5

 pred f is_integrable_on C means for a,b be Real, x,y be PartFunc of REAL , REAL , Z be Subset of REAL , u0,v0 be 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 + ( (#) 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

 definition

 let f be PartFunc of COMPLEX , COMPLEX ;

 let C be C1-curve;

 :: INTEGR1C:def6

 pred f is_bounded_on C means for a,b be Real, x,y be PartFunc of REAL , REAL , Z be Subset of REAL , u0,v0 be 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 + ( (#) 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

 begin

 theorem :: INTEGR1C:1

 for f,g be PartFunc of COMPLEX , COMPLEX , C be 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 , C be C1-curve such that

 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;

 consider a,b be Real, x,y be PartFunc of REAL , REAL , Z be 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 + ( (#) y)) | [.a, b.]) by Def3;

 reconsider a, b as Real;

 consider uf0,vf0 be 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)) * )) by Def2;

 consider ug0,vg0 be 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)) * )) 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 be 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)) * )) 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 be object st x0 in ( dom u0) holds x0 in (( dom uf0) /\ ( dom ug0))

 proof

 let x0 be object such that

 A14: x0 in ( dom u0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re (f + g))) by A15, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (( Re f) + ( Re g))) by MESFUN6C: 5;

 then ( R2-to-C . R2) in (( dom ( Re f)) /\ ( dom ( Re g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Re f)) & ( R2-to-C . R2) in ( dom ( Re g)) by XBOOLE_0:def 4;

 then R2 in ( dom (( Re f) * R2-to-C )) & R2 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 thesis by XBOOLE_0:def 4;

 end;

 for x0 be object st x0 in (( dom uf0) /\ ( dom ug0)) holds x0 in ( dom u0)

 proof

 let x0 be object such that

 A17: x0 in (( dom uf0) /\ ( dom ug0));



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re f)) by A19, FUNCT_1: 11;

 R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re g)) by A20, FUNCT_1: 11;

 then ( R2-to-C . R2) in (( dom ( Re f)) /\ ( dom ( Re g))) by A21, XBOOLE_0:def 4;

 then ( R2-to-C . R2) in ( dom (( Re f) + ( Re g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Re (f + g))) by MESFUN6C: 5;

 then R2 in ( dom (( Re (f + g)) * R2-to-C )) by A21, FUNCT_1: 11;

 hence thesis by A8, A19, FUNCT_1: 11;

 end;

 hence thesis by A13, TARSKI: 2;

 end;

 for x0 be object st x0 in ( dom (u0 (#) (x `| Z))) holds ((u0 (#) (x `| Z)) . x0) = (((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0)

 proof

 let x0 be object such that

 A22: x0 in ( dom (u0 (#) (x `| Z)));

 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re (f + g))) by A24, FUNCT_1: 11;

 set c0 = ( R2-to-C . R2);



 A26: (u0 . x0) = ((( Re (f + g)) * R2-to-C ) . R2) by A8, A23, FUNCT_1: 12

 .= (( Re (f + g)) . c0) by A24, FUNCT_1: 12

 .= ((( Re f) + ( Re g)) . c0) by MESFUN6C: 5;



 A27: c0 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:>) & R2 in ( dom (( Re f) * R2-to-C )) by A3, FUNCT_1: 11;



 A30: (uf0 . x0) = ((( Re f) * R2-to-C ) . R2) by A3, A28, FUNCT_1: 12

 .= (( Re f) . c0) by A29, FUNCT_1: 12;



 A31: x0 in ( dom <:x, y:>) & R2 in ( dom (( Re g) * R2-to-C )) by A4, A28, FUNCT_1: 11;



 A32: (ug0 . x0) = ((( Re g) * R2-to-C ) . R2) by A4, A28, FUNCT_1: 12

 .= (( Re g) . c0) 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) . c0) * ((x `| Z) . x0)) by A30, VALUED_1:def 4;



 A35: ((ug0 (#) (x `| Z)) . x0) = ((( Re g) . c0) * ((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) . c0) + (( Re g) . c0)) * ((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 thesis;

 end;

 hence thesis by A10, A11, A12, FUNCT_1: 2;

 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 be object st x0 in ( dom v0) holds x0 in (( dom vf0) /\ ( dom vg0))

 proof

 let x0 be object such that

 A41: x0 in ( dom v0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im (f + g))) by A42, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (( Im f) + ( Im g))) by MESFUN6C: 5;

 then ( R2-to-C . R2) in (( dom ( Im f)) /\ ( dom ( Im g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Im f)) & ( R2-to-C . R2) in ( dom ( Im g)) by XBOOLE_0:def 4;

 then R2 in ( dom (( Im f) * R2-to-C )) & R2 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 thesis by XBOOLE_0:def 4;

 end;

 for x0 be object st x0 in (( dom vf0) /\ ( dom vg0)) holds x0 in ( dom v0)

 proof

 let x0 be object such that

 A44: x0 in (( dom vf0) /\ ( dom vg0));



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im f)) by A46, FUNCT_1: 11;

 R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im g)) by A47, FUNCT_1: 11;

 then ( R2-to-C . R2) in (( dom ( Im f)) /\ ( dom ( Im g))) by A48, XBOOLE_0:def 4;

 then ( R2-to-C . R2) in ( dom (( Im f) + ( Im g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Im (f + g))) by MESFUN6C: 5;

 then R2 in ( dom (( Im (f + g)) * R2-to-C )) by A48, FUNCT_1: 11;

 hence thesis by A8, A46, FUNCT_1: 11;

 end;

 hence thesis by A40, TARSKI: 2;

 end;

 for x0 be object st x0 in ( dom (v0 (#) (x `| Z))) holds ((v0 (#) (x `| Z)) . x0) = (((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0)

 proof

 let x0 be object such that

 A49: x0 in ( dom (v0 (#) (x `| Z)));

 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im (f + g))) by A51, FUNCT_1: 11;

 set c0 = ( R2-to-C . R2);



 A53: (v0 . x0) = ((( Im (f + g)) * R2-to-C ) . R2) by A8, A50, FUNCT_1: 12

 .= (( Im (f + g)) . c0) by A51, FUNCT_1: 12

 .= ((( Im f) + ( Im g)) . c0) by MESFUN6C: 5;



 A54: c0 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:>) & R2 in ( dom (( Im f) * R2-to-C )) by A3, FUNCT_1: 11;



 A57: (vf0 . x0) = ((( Im f) * R2-to-C ) . R2) by A3, A55, FUNCT_1: 12

 .= (( Im f) . c0) by A56, FUNCT_1: 12;



 A58: x0 in ( dom <:x, y:>) & R2 in ( dom (( Im g) * R2-to-C )) by A4, A55, FUNCT_1: 11;



 A59: (vg0 . x0) = ((( Im g) * R2-to-C ) . R2) by A4, A55, FUNCT_1: 12

 .= (( Im g) . c0) 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) . c0) * ((x `| Z) . x0)) by A57, VALUED_1:def 4;



 A62: ((vg0 (#) (x `| Z)) . x0) = ((( Im g) . c0) * ((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) . c0) + (( Im g) . c0)) * ((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 thesis;

 end;

 hence thesis by A37, A38, A39, FUNCT_1: 2;

 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 be object st x0 in ( dom u0) holds x0 in (( dom uf0) /\ ( dom ug0))

 proof

 let x0 be object such that

 A68: x0 in ( dom u0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re (f + g))) by A69, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (( Re f) + ( Re g))) by MESFUN6C: 5;

 then ( R2-to-C . R2) in (( dom ( Re f)) /\ ( dom ( Re g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Re f)) & ( R2-to-C . R2) in ( dom ( Re g)) by XBOOLE_0:def 4;

 then R2 in ( dom (( Re f) * R2-to-C )) & R2 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 thesis by XBOOLE_0:def 4;

 end;

 for x0 be object st x0 in (( dom uf0) /\ ( dom ug0)) holds x0 in ( dom u0)

 proof

 let x0 be object such that

 A71: x0 in (( dom uf0) /\ ( dom ug0));



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re f)) by A73, FUNCT_1: 11;

 R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re g)) by A74, FUNCT_1: 11;

 then ( R2-to-C . R2) in (( dom ( Re f)) /\ ( dom ( Re g))) by A75, XBOOLE_0:def 4;

 then ( R2-to-C . R2) in ( dom (( Re f) + ( Re g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Re (f + g))) by MESFUN6C: 5;

 then R2 in ( dom (( Re (f + g)) * R2-to-C )) by A75, FUNCT_1: 11;

 hence thesis by A8, A73, FUNCT_1: 11;

 end;

 hence thesis by A67, TARSKI: 2;

 end;

 for x0 be object st x0 in ( dom (u0 (#) (y `| Z))) holds ((u0 (#) (y `| Z)) . x0) = (((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0)

 proof

 let x0 be object such that

 A76: x0 in ( dom (u0 (#) (y `| Z)));

 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re (f + g))) by A78, FUNCT_1: 11;

 set c0 = ( R2-to-C . R2);



 A80: (u0 . x0) = ((( Re (f + g)) * R2-to-C ) . R2) by A8, A77, FUNCT_1: 12

 .= (( Re (f + g)) . c0) by A78, FUNCT_1: 12

 .= ((( Re f) + ( Re g)) . c0) by MESFUN6C: 5;



 A81: c0 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:>) & R2 in ( dom (( Re f) * R2-to-C )) by A3, FUNCT_1: 11;



 A84: (uf0 . x0) = ((( Re f) * R2-to-C ) . R2) by A3, A82, FUNCT_1: 12

 .= (( Re f) . c0) by A83, FUNCT_1: 12;



 A85: x0 in ( dom <:x, y:>) & R2 in ( dom (( Re g) * R2-to-C )) by A4, A82, FUNCT_1: 11;



 A86: (ug0 . x0) = ((( Re g) * R2-to-C ) . R2) by A4, A82, FUNCT_1: 12

 .= (( Re g) . c0) 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) . c0) * ((y `| Z) . x0)) by A84, VALUED_1:def 4;



 A89: ((ug0 (#) (y `| Z)) . x0) = ((( Re g) . c0) * ((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) . c0) + (( Re g) . c0)) * ((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 thesis;

 end;

 hence thesis by A64, A65, A66, FUNCT_1: 2;

 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 be object st x0 in ( dom v0) holds x0 in (( dom vf0) /\ ( dom vg0))

 proof

 let x0 be object such that

 A95: x0 in ( dom v0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im (f + g))) by A96, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (( Im f) + ( Im g))) by MESFUN6C: 5;

 then ( R2-to-C . R2) in (( dom ( Im f)) /\ ( dom ( Im g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Im f)) & ( R2-to-C . R2) in ( dom ( Im g)) by XBOOLE_0:def 4;

 then R2 in ( dom (( Im f) * R2-to-C )) & R2 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 thesis by XBOOLE_0:def 4;

 end;

 for x0 be object st x0 in (( dom vf0) /\ ( dom vg0)) holds x0 in ( dom v0)

 proof

 let x0 be object such that

 A98: x0 in (( dom vf0) /\ ( dom vg0));



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im f)) by A100, FUNCT_1: 11;

 R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im g)) by A101, FUNCT_1: 11;

 then ( R2-to-C . R2) in (( dom ( Im f)) /\ ( dom ( Im g))) by A102, XBOOLE_0:def 4;

 then ( R2-to-C . R2) in ( dom (( Im f) + ( Im g))) by VALUED_1:def 1;

 then ( R2-to-C . R2) in ( dom ( Im (f + g))) by MESFUN6C: 5;

 then R2 in ( dom (( Im (f + g)) * R2-to-C )) by A102, FUNCT_1: 11;

 hence thesis by A8, A100, FUNCT_1: 11;

 end;

 hence thesis by A94, TARSKI: 2;

 end;

 for x0 be object st x0 in ( dom (v0 (#) (y `| Z))) holds ((v0 (#) (y `| Z)) . x0) = (((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0)

 proof

 let x0 be object such that

 A103: x0 in ( dom (v0 (#) (y `| Z)));

 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im (f + g))) by A105, FUNCT_1: 11;

 set c0 = ( R2-to-C . R2);



 A107: (v0 . x0) = ((( Im (f + g)) * R2-to-C ) . R2) by A8, A104, FUNCT_1: 12

 .= (( Im (f + g)) . c0) by A105, FUNCT_1: 12

 .= ((( Im f) + ( Im g)) . c0) by MESFUN6C: 5;



 A108: c0 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:>) & R2 in ( dom (( Im f) * R2-to-C )) by A3, FUNCT_1: 11;



 A111: (vf0 . x0) = ((( Im f) * R2-to-C ) . R2) by A3, A109, FUNCT_1: 12

 .= (( Im f) . c0) by A110, FUNCT_1: 12;



 A112: x0 in ( dom <:x, y:>) & R2 in ( dom (( Im g) * R2-to-C )) by A4, A109, FUNCT_1: 11;



 A113: (vg0 . x0) = ((( Im g) * R2-to-C ) . R2) by A4, A109, FUNCT_1: 12

 .= (( Im g) . c0) 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) . c0) * ((y `| Z) . x0)) by A111, VALUED_1:def 4;



 A116: ((vg0 (#) (y `| Z)) . x0) = ((( Im g) . c0) * ((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) . c0) + (( Im g) . c0)) * ((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 thesis;

 end;

 hence thesis by A91, A92, A93, FUNCT_1: 2;

 end;



 A117: [.a, b.] c= ( dom uf0)

 proof

 let x0 be object such that

 A118: x0 in [.a, b.];



 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);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A121, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A123: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A120, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A2, A118, XBOOLE_0:def 4;

 then

 A124: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A125: [xx0, yx0] 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 + ( (#) y)) . x0) by A118, A2, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A124, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A125, A126, Def1

 .= ( R2-to-C . R2) by A121, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom f) by A1, A119;

 then ( R2-to-C . R2) in ( dom ( Re f)) by COMSEQ_3:def 3;

 then R2 in ( dom (( Re f) * R2-to-C )) by A123, FUNCT_1: 11;

 hence thesis by A3, A122, FUNCT_1: 11;

 end;



 A127: [.a, b.] c= ( dom vf0)

 proof

 let x0 be object such that

 A128: x0 in [.a, b.];



 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);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A131, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A133: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A130, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A2, A128, XBOOLE_0:def 4;

 then

 A134: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A135: [xx0, yx0] 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 + ( (#) y)) . x0) by A128, A2, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A134, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A135, A136, Def1

 .= ( R2-to-C . R2) by A131, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom f) by A1, A129;

 then ( R2-to-C . R2) in ( dom ( Im f)) by COMSEQ_3:def 4;

 then R2 in ( dom (( Im f) * R2-to-C )) by A133, FUNCT_1: 11;

 hence thesis by A3, A132, FUNCT_1: 11;

 end;



 A137: [.a, b.] c= ( dom ug0)

 proof

 let x0 be object such that

 A138: x0 in [.a, b.];



 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);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A141, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A143: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A140, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A2, A138, XBOOLE_0:def 4;

 then

 A144: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A145: [xx0, yx0] 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 + ( (#) y)) . x0) by A138, A2, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A144, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A145, A146, Def1

 .= ( R2-to-C . R2) by A141, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom g) by A1, A139;

 then ( R2-to-C . R2) in ( dom ( Re g)) by COMSEQ_3:def 3;

 then R2 in ( dom (( Re g) * R2-to-C )) by A143, FUNCT_1: 11;

 hence thesis by A4, A142, FUNCT_1: 11;

 end;



 A147: [.a, b.] c= ( dom vg0)

 proof

 let x0 be object such that

 A148: x0 in [.a, b.];



 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);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A151, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A153: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A150, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A2, A148, XBOOLE_0:def 4;

 then

 A154: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A155: [xx0, yx0] 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 + ( (#) y)) . x0) by A148, A2, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A154, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A155, A156, Def1

 .= ( R2-to-C . R2) by A151, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom g) by A1, A149;

 then ( R2-to-C . R2) in ( dom ( Im g)) by COMSEQ_3:def 4;

 then R2 in ( dom (( Im g) * R2-to-C )) by A153, FUNCT_1: 11;

 hence thesis by A4, A152, FUNCT_1: 11;

 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 thesis by A2, A158, A159, XBOOLE_1: 19;

 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 thesis by A2, A161, A162, XBOOLE_1: 19;

 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 thesis by A2, A164, A165, XBOOLE_1: 19;

 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 thesis by A2, A167, A168, XBOOLE_1: 19;

 end;

 reconsider a, b as Real;



 A169: ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) is_integrable_on ['a, b'] by A1, A2;



 A170: ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))) is_integrable_on ['a, b'] by A1, A2;



 A171: ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) is_integrable_on ['a, b'] by A1, A2;



 A172: ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z))) is_integrable_on ['a, b'] by A1, A2;



 A173: (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) | ['a, b']) is bounded by A1, A2;



 A174: (((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z))) | ['a, b']) is bounded by A1, A2;



 A175: (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) | ['a, b']) is bounded by A1, A2;



 A176: (((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z))) | ['a, b']) is bounded by A1, A2;

 ( 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)) * )) 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)) * )) 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)) * )) 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)) * )) 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)) * )) 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)) * )) 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)) * )) 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)) * )) 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))) * )) by A2, A163, A166, A171, A172, A175, A176, INTEGRA6: 12

 .= (( integral (f,C)) + ( integral (g,C))) by A4, A5, A3;

 hence thesis;

 end;

 theorem :: INTEGR1C:2

 for f be PartFunc of COMPLEX , COMPLEX , C be C1-curve st ( rng C) c= ( dom f) & f is_integrable_on C & f is_bounded_on C holds for r be Real holds ( integral ((r (#) f),C)) = (r * ( integral (f,C)))

 proof

 let f be PartFunc of COMPLEX , COMPLEX , C be C1-curve such that

 A1: ( rng C) c= ( dom f) & f is_integrable_on C & f is_bounded_on C;

 let r be Real;

 consider a,b be Real, x,y be PartFunc of REAL , REAL , Z be 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 + ( (#) y)) | [.a, b.]) by Def3;

 reconsider a, b as Real;

 consider uf0,vf0 be 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)) * )) by Def2;



 A4: ( dom (r (#) f)) = ( dom f) by VALUED_1:def 5;

 consider u0,v0 be 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)) * )) by Def2;



 A6: ( dom u0) = ( dom uf0)

 proof



 A7: for x0 be object st x0 in ( dom u0) holds x0 in ( dom uf0)

 proof

 let x0 be object such that

 A8: x0 in ( dom u0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re (r (#) f))) by A9, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (r (#) ( Re f))) by MESFUN6C: 2;

 then ( R2-to-C . R2) in ( dom ( Re f)) by VALUED_1:def 5;

 then R2 in ( dom (( Re f) * R2-to-C )) by A10, FUNCT_1: 11;

 hence thesis by A3, A9, FUNCT_1: 11;

 end;

 for x0 be object st x0 in ( dom uf0) holds x0 in ( dom u0)

 proof

 let x0 be object such that

 A11: x0 in ( dom uf0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Re f)) by A12, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (r (#) ( Re f))) by VALUED_1:def 5;

 then ( R2-to-C . R2) in ( dom ( Re (r (#) f))) by MESFUN6C: 2;

 then R2 in ( dom (( Re (r (#) f)) * R2-to-C )) by A13, FUNCT_1: 11;

 hence thesis by A5, A12, FUNCT_1: 11;

 end;

 hence thesis by A7, TARSKI: 2;

 end;



 A14: ( dom v0) = ( dom vf0)

 proof



 A15: for x0 be object st x0 in ( dom v0) holds x0 in ( dom vf0)

 proof

 let x0 be object such that

 A16: x0 in ( dom v0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im (r (#) f))) by A17, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (r (#) ( Im f))) by MESFUN6C: 2;

 then ( R2-to-C . R2) in ( dom ( Im f)) by VALUED_1:def 5;

 then R2 in ( dom (( Im f) * R2-to-C )) by A18, FUNCT_1: 11;

 hence thesis by A3, A17, FUNCT_1: 11;

 end;

 for x0 be object st x0 in ( dom vf0) holds x0 in ( dom v0)

 proof

 let x0 be object such that

 A19: x0 in ( dom vf0);



 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: R2 in ( dom R2-to-C ) & ( R2-to-C . R2) in ( dom ( Im f)) by A20, FUNCT_1: 11;

 then ( R2-to-C . R2) in ( dom (r (#) ( Im f))) by VALUED_1:def 5;

 then ( R2-to-C . R2) in ( dom ( Im (r (#) f))) by MESFUN6C: 2;

 then R2 in ( dom (( Im (r (#) f)) * R2-to-C )) by A21, FUNCT_1: 11;

 hence thesis by A5, A20, FUNCT_1: 11;

 end;

 hence thesis by A15, TARSKI: 2;

 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 be object st x0 in ( dom (u0 (#) (x `| Z))) holds ((u0 (#) (x `| Z)) . x0) = ((r (#) (uf0 (#) (x `| Z))) . x0)

 proof

 let x0 be object such that

 A26: x0 in ( dom (u0 (#) (x `| Z)));



 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 . R2);



 A30: (u0 . x0) = ((( Re (r (#) f)) * R2-to-C ) . R2) by A5, A28, FUNCT_1: 12

 .= (( Re (r (#) f)) . c0) by A29, FUNCT_1: 12

 .= ((r (#) ( Re f)) . c0) by MESFUN6C: 2;

 x0 in ( dom uf0) by A6, A27, XBOOLE_0:def 4;

 then

 A31: x0 in ( dom <:x, y:>) & R2 in ( dom (( Re f) * R2-to-C )) by A3, FUNCT_1: 11;



 A32: (uf0 . x0) = ((( Re f) * R2-to-C ) . R2) by A3, A6, A28, FUNCT_1: 12

 .= (( Re f) . c0) 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) . c0)) * ((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 thesis;

 end;

 hence thesis by A6, A23, A24, FUNCT_1: 2;

 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 be object st x0 in ( dom (v0 (#) (x `| Z))) holds ((v0 (#) (x `| Z)) . x0) = ((r (#) (vf0 (#) (x `| Z))) . x0)

 proof

 let x0 be object such that

 A39: x0 in ( dom (v0 (#) (x `| Z)));



 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 . R2);



 A43: (v0 . x0) = ((( Im (r (#) f)) * R2-to-C ) . R2) by A5, A41, FUNCT_1: 12

 .= (( Im (r (#) f)) . c0) by A42, FUNCT_1: 12

 .= ((r (#) ( Im f)) . c0) by MESFUN6C: 2;

 x0 in ( dom vf0) by A14, A40, XBOOLE_0:def 4;

 then

 A44: x0 in ( dom <:x, y:>) & R2 in ( dom (( Im f) * R2-to-C )) by A3, FUNCT_1: 11;



 A45: (vf0 . x0) = ((( Im f) * R2-to-C ) . R2) by A3, A14, A41, FUNCT_1: 12

 .= (( Im f) . c0) 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) . c0)) * ((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 thesis;

 end;

 hence thesis by A14, A36, A37, FUNCT_1: 2;

 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 be object st x0 in ( dom (u0 (#) (y `| Z))) holds ((u0 (#) (y `| Z)) . x0) = ((r (#) (uf0 (#) (y `| Z))) . x0)

 proof

 let x0 be object such that

 A52: x0 in ( dom (u0 (#) (y `| Z)));



 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 . R2);



 A56: (u0 . x0) = ((( Re (r (#) f)) * R2-to-C ) . R2) by A5, A54, FUNCT_1: 12

 .= (( Re (r (#) f)) . c0) by A55, FUNCT_1: 12

 .= ((r (#) ( Re f)) . c0) by MESFUN6C: 2;

 x0 in ( dom uf0) by A6, A53, XBOOLE_0:def 4;

 then

 A57: x0 in ( dom <:x, y:>) & R2 in ( dom (( Re f) * R2-to-C )) by A3, FUNCT_1: 11;



 A58: (uf0 . x0) = ((( Re f) * R2-to-C ) . R2) by A3, A6, A54, FUNCT_1: 12

 .= (( Re f) . c0) 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) . c0)) * ((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 thesis;

 end;

 hence thesis by A6, A49, A50, FUNCT_1: 2;

 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 be object st x0 in ( dom (v0 (#) (y `| Z))) holds ((v0 (#) (y `| Z)) . x0) = ((r (#) (vf0 (#) (y `| Z))) . x0)

 proof

 let x0 be object such that

 A65: x0 in ( dom (v0 (#) (y `| Z)));



 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 . R2);



 A69: (v0 . x0) = ((( Im (r (#) f)) * R2-to-C ) . R2) by A5, A67, FUNCT_1: 12

 .= (( Im (r (#) f)) . c0) by A68, FUNCT_1: 12

 .= ((r (#) ( Im f)) . c0) by MESFUN6C: 2;

 x0 in ( dom vf0) by A14, A66, XBOOLE_0:def 4;

 then

 A70: x0 in ( dom <:x, y:>) & R2 in ( dom (( Im f) * R2-to-C )) by A3, FUNCT_1: 11;



 A71: (vf0 . x0) = ((( Im f) * R2-to-C ) . R2) by A3, A14, A67, FUNCT_1: 12

 .= (( Im f) . c0) 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) . c0)) * ((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 thesis;

 end;

 hence thesis by A14, A62, A63, FUNCT_1: 2;

 end;



 A74: [.a, b.] c= ( dom uf0)

 proof

 let x0 be object such that

 A75: x0 in [.a, b.];



 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);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A78, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A80: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A77, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A2, A75, XBOOLE_0:def 4;

 then

 A81: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A82: [xx0, yx0] 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 + ( (#) y)) . x0) by A75, A2, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A81, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A82, A83, Def1

 .= ( R2-to-C . R2) by A78, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom f) by A1, A76;

 then ( R2-to-C . R2) in ( dom ( Re f)) by COMSEQ_3:def 3;

 then R2 in ( dom (( Re f) * R2-to-C )) by A80, FUNCT_1: 11;

 hence thesis by A3, A79, FUNCT_1: 11;

 end;



 A84: [.a, b.] c= ( dom vf0)

 proof

 let x0 be object such that

 A85: x0 in [.a, b.];



 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);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A88, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A90: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A87, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A2, A85, XBOOLE_0:def 4;

 then

 A91: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A92: [xx0, yx0] 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 + ( (#) y)) . x0) by A85, A2, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A91, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A92, A93, Def1

 .= ( R2-to-C . R2) by A88, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom f) by A1, A86;

 then ( R2-to-C . R2) in ( dom ( Im f)) by COMSEQ_3:def 4;

 then R2 in ( dom (( Im f) * R2-to-C )) by A90, FUNCT_1: 11;

 hence thesis by A3, A89, FUNCT_1: 11;

 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 thesis by A2, A95, A96, XBOOLE_1: 19;

 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 thesis by A2, A98, A99, XBOOLE_1: 19;

 end;

 reconsider a, b as Real;



 A100: ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) is_integrable_on ['a, b'] by A1, A2;



 A101: ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) is_integrable_on ['a, b'] by A1, A2;



 A102: (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))) | ['a, b']) is bounded by A1, A2;



 A103: (((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z))) | ['a, b']) is bounded by A1, A2;

 ( 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)) * )) 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)) * )) by RFUNCT_1: 18

 .= (( integral ((r (#) ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))),a,b)) + (( integral ((r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b)) * )) by RFUNCT_1: 16

 .= ((r * ( integral (((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z))),a,b))) + (( integral ((r (#) ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))),a,b)) * )) 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))) * )) 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)) * )))

 .= (r * ( integral (f,C))) by A1, A2, A3, Def4;

 hence thesis;

 end;

 begin

 theorem :: INTEGR1C:3

 for f be PartFunc of COMPLEX , COMPLEX , C,C1,C2 be C1-curve, a,b,d be 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 st t in ( dom C1) holds (C . t) = (C1 . t)) & (for t 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 , C,C1,C2 be C1-curve, a,b,d be Real such that

 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 st t in ( dom C1) holds (C . t) = (C1 . t)) & (for t st t in ( dom C2) holds (C . t) = (C2 . t));



 A2: a <= d & d <= b by A1, XXREAL_1: 1;

 consider a0,b0 be Real, x,y be PartFunc of REAL , REAL , Z be Subset of REAL such that

 A3: a0 <= b0 & [.a0, b0.] = ( dom C) & [.a0, b0.] c= ( dom x) & [.a0, b0.] c= ( dom y) & Z is open & [.a0, b0.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z & (x `| Z) is continuous & (y `| Z) is continuous & C = ((x + ( (#) y)) | [.a0, b0.]) by Def3;



 A4: a0 = a & b0 = b

 proof



 thus a0 = ( inf [.a0, b0.]) by A3, XXREAL_2: 25

 .= a by A1, A3, XXREAL_2: 25;



 thus b0 = ( sup [.a0, b0.]) by A3, XXREAL_2: 29

 .= b by A1, A3, XXREAL_2: 29;

 end;

 consider u0,v0 be PartFunc of REAL , REAL such that

 A5: u0 = ((( Re f) * R2-to-C ) * <:x, y:>) & v0 = ((( Im f) * R2-to-C ) * <:x, y:>) & ( integral (f,x,y,a,b,Z)) = (( integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + (( integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * )) by Def2;

 consider a1,b1 be Real, x1,y1 be PartFunc of REAL , REAL , Z1 be Subset of REAL such that

 A6: a1 <= b1 & [.a1, b1.] = ( dom C1) & [.a1, b1.] c= ( dom x1) & [.a1, b1.] c= ( dom y1) & Z1 is open & [.a1, b1.] c= Z1 & x1 is_differentiable_on Z1 & y1 is_differentiable_on Z1 & (x1 `| Z1) is continuous & (y1 `| Z1) is continuous & C1 = ((x1 + ( (#) y1)) | [.a1, b1.]) by Def3;



 A7: a1 = a & b1 = d

 proof



 thus a1 = ( inf [.a1, b1.]) by A6, XXREAL_2: 25

 .= a by A2, A1, A6, XXREAL_2: 25;



 thus b1 = ( sup [.a1, b1.]) by A6, XXREAL_2: 29

 .= d by A2, A1, A6, XXREAL_2: 29;

 end;



 A8: ( rng C1) c= ( dom f)

 proof



 A9: [.a, d.] c= [.a, b.] by A2, XXREAL_1: 34;

 for y0 be object st y0 in ( rng C1) holds y0 in ( rng C)

 proof

 let y0 be object such that

 A10: y0 in ( rng C1);

 consider x0 be object such that

 A11: x0 in ( dom C1) & y0 = (C1 . x0) by A10, FUNCT_1:def 3;

 (C1 . x0) = (C . x0) by A1, A11;

 hence thesis by A1, A9, A11, FUNCT_1: 3;

 end;

 then ( rng C1) c= ( rng C);

 hence thesis by A1;

 end;

 consider a2,b2 be Real, x2,y2 be PartFunc of REAL , REAL , Z2 be Subset of REAL such that

 A12: a2 <= b2 & [.a2, b2.] = ( dom C2) & [.a2, b2.] c= ( dom x2) & [.a2, b2.] c= ( dom y2) & Z2 is open & [.a2, b2.] c= Z2 & x2 is_differentiable_on Z2 & y2 is_differentiable_on Z2 & (x2 `| Z2) is continuous & (y2 `| Z2) is continuous & C2 = ((x2 + ( (#) y2)) | [.a2, b2.]) by Def3;



 A13: a2 = d & b2 = b

 proof



 thus a2 = ( inf [.a2, b2.]) by A12, XXREAL_2: 25

 .= d by A2, A1, A12, XXREAL_2: 25;



 thus b2 = ( sup [.a2, b2.]) by A12, XXREAL_2: 29

 .= b by A2, A1, A12, XXREAL_2: 29;

 end;

 ( rng C2) c= ( dom f)

 proof



 A14: [.d, b.] c= [.a, b.] by A2, XXREAL_1: 34;

 for y0 be object st y0 in ( rng C2) holds y0 in ( rng C)

 proof

 let y0 be object such that

 A15: y0 in ( rng C2);

 consider x0 be object such that

 A16: x0 in ( dom C2) & y0 = (C2 . x0) by A15, FUNCT_1:def 3;

 (C2 . x0) = (C . x0) by A1, A16;

 hence thesis by A1, A14, A16, FUNCT_1: 3;

 end;

 then ( rng C2) c= ( rng C);

 hence thesis by A1;

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

 proof

 let x0 be object such that

 A20: x0 in [.a, b.];



 A21: (C . x0) in ( rng C) by A3, A4, A20, FUNCT_1: 3;



 A22: x0 in ( dom x) & x0 in ( dom y) by A3, A4, A20;



 A23: x0 in (( dom x) /\ ( dom y)) by A3, A4, A20, XBOOLE_0:def 4;

 then

 A24: x0 in ( dom <:x, y:>) by FUNCT_3:def 7;

 set R2 = ( <:x, y:> . x0);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A23, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A25: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A22, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A3, A4, A20, XBOOLE_0:def 4;

 then

 A26: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A27: [xx0, yx0] in [: REAL , REAL :] by ZFMISC_1:def 2;



 A28: (x . x0) = ( [(x . x0), (y . x0)] `1 ) & (y . x0) = ( [(x . x0), (y . x0)] `2 );

 (C . x0) = ((x + ( (#) y)) . x0) by A20, A3, A4, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A26, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A27, A28, Def1

 .= ( R2-to-C . R2) by A23, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom f) by A1, A21;

 then ( R2-to-C . R2) in ( dom ( Re f)) by COMSEQ_3:def 3;

 then R2 in ( dom (( Re f) * R2-to-C )) by A25, FUNCT_1: 11;

 hence thesis by A5, A24, FUNCT_1: 11;

 end;

 hence thesis by A18;

 end;



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

 proof

 for x0 be object st x0 in [.a, b.] holds x0 in ( dom v0)

 proof

 let x0 be object such that

 A30: x0 in [.a, b.];



 A31: (C . x0) in ( rng C) by A3, A4, A30, FUNCT_1: 3;



 A32: x0 in ( dom x) & x0 in ( dom y) by A3, A4, A30;



 A33: x0 in (( dom x) /\ ( dom y)) by A3, A4, A30, XBOOLE_0:def 4;

 then

 A34: x0 in ( dom <:x, y:>) by FUNCT_3:def 7;

 set R2 = ( <:x, y:> . x0);

 reconsider xx0 = (x . x0), yx0 = (y . x0) as Element of REAL by XREAL_0:def 1;

 R2 = [xx0, yx0] by A33, FUNCT_3: 48;

 then R2 in [: REAL , REAL :] by ZFMISC_1:def 2;

 then

 A35: R2 in ( dom R2-to-C ) by FUNCT_2:def 1;

 x0 in ( dom ( (#) y)) by A32, VALUED_1:def 5;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by A3, A4, A30, XBOOLE_0:def 4;

 then

 A36: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;



 A37: [xx0, yx0] in [: REAL , REAL :] by ZFMISC_1:def 2;



 A38: (x . x0) = ( [(x . x0), (y . x0)] `1 ) & (y . x0) = ( [(x . x0), (y . x0)] `2 );

 (C . x0) = ((x + ( (#) y)) . x0) by A30, A3, A4, FUNCT_1: 49

 .= ((x . x0) + (( (#) y) . x0)) by A36, VALUED_1:def 1

 .= ((x . x0) + ( * (y . x0))) by VALUED_1: 6

 .= ( R2-to-C . [xx0, yx0]) by A37, A38, Def1

 .= ( R2-to-C . R2) by A33, FUNCT_3: 48;

 then ( R2-to-C . R2) in ( dom f) by A1, A31;

 then ( R2-to-C . R2) in ( dom ( Im f)) by COMSEQ_3:def 4;

 then R2 in ( dom (( Im f) * R2-to-C )) by A35, FUNCT_1: 11;

 hence thesis by A5, A34, FUNCT_1: 11;

 end;

 hence thesis by A18;

 end;



 A39: ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))) is_integrable_on ['a, b'] & ((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))) is_integrable_on ['a, b'] by A1, A3;



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



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

 proof



 A42: ( dom ((u0 (#) (x `| Z)) - (v0 (#) (y `| Z)))) = (( dom (u0 (#) (x `| Z))) /\ ( dom (v0 (#) (y `| Z)))) by VALUED_1: 12

 .= ((( dom u0) /\ ( dom (x `| Z))) /\ ( dom (v0 (#) (y `| Z)))) by VALUED_1:def 4

 .= ((( dom u0) /\ ( dom (x `| Z))) /\ (( dom v0) /\ ( dom (y `| Z)))) by VALUED_1:def 4

 .= ((( dom u0) /\ Z) /\ (( dom v0) /\ ( dom (y `| Z)))) by A3, FDIFF_1:def 7

 .= ((( dom u0) /\ Z) /\ (( dom v0) /\ Z)) by A3, FDIFF_1:def 7

 .= (( dom u0) /\ (Z /\ (( dom v0) /\ Z))) by XBOOLE_1: 16

 .= (( dom u0) /\ ((Z /\ Z) /\ ( dom v0))) by XBOOLE_1: 16

 .= ((( dom u0) /\ ( dom v0)) /\ Z) by XBOOLE_1: 16;



 A43: ['a, b'] c= (( dom u0) /\ ( dom v0)) by A19, A29, XBOOLE_1: 19;

 ['a, b'] c= Z by A1, A3, INTEGRA5:def 3;

 hence thesis by A42, A43, XBOOLE_1: 19;

 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 thesis by A45, A46, XBOOLE_1: 19;

 end;



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



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



 A49: ( integral (f,x,y,a,d,Z)) = ( integral (f,x1,y1,a,d,Z1))

 proof

 reconsider Z3 = (Z /\ Z1) as Subset of REAL ;

 reconsider ZZ = Z, ZZ1 = Z1 as Subset of R^1 by TOPMETR: 17;

 ZZ is open & ZZ1 is open by A3, A6, BORSUK_5: 39;

 then (ZZ /\ ZZ1) is open by TOPS_1: 11;

 then

 A50: Z3 is open by BORSUK_5: 39;



 A51: [.a, d.] c= [.a, b.] by A2, XXREAL_1: 34;

 then

 A52: [.a, d.] c= ( dom x) & [.a, d.] c= ( dom y) by A3, A4;



 A53: (x | [.a, d.]) = (x1 | [.a, d.])

 proof



 A54: ( dom (x | [.a, d.])) = (( dom x) /\ [.a, d.]) by RELAT_1: 61

 .= [.a, d.] by A3, A4, A51, XBOOLE_1: 1, XBOOLE_1: 28

 .= (( dom x1) /\ [.a, d.]) by A6, A7, XBOOLE_1: 28

 .= ( dom (x1 | [.a, d.])) by RELAT_1: 61;

 for x0 be object st x0 in ( dom (x | [.a, d.])) holds ((x | [.a, d.]) . x0) = ((x1 | [.a, d.]) . x0)

 proof

 let x0 be object such that

 A55: x0 in ( dom (x | [.a, d.]));



 A56: ( dom (x | [.a, d.])) = (( dom x) /\ [.a, d.]) by RELAT_1: 61

 .= [.a, d.] by A51, A3, A4, XBOOLE_1: 1, XBOOLE_1: 28;

 [.a, d.] c= (( dom x1) /\ ( dom y1)) by A6, A7, XBOOLE_1: 19;

 then x0 in (( dom x1) /\ ( dom y1)) by A55, A56;

 then x0 in (( dom x1) /\ ( dom ( (#) y1))) by VALUED_1:def 5;

 then

 A57: x0 in ( dom (x1 + ( (#) y1))) by VALUED_1:def 1;

 [.a, d.] c= (( dom x) /\ ( dom y)) by A52, XBOOLE_1: 19;

 then x0 in (( dom x) /\ ( dom y)) by A55, A56;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by VALUED_1:def 5;

 then

 A58: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;

 reconsider t = x0 as Element of REAL by A55;



 A59: (C . t) = (C1 . t) by A1, A55, A56;



 A60: (C . t) = ((x + ( (#) y)) . t) by A3, A4, A51, A55, A56, FUNCT_1: 49;



 A61: (C1 . t) = ((x1 + ( (#) y1)) . t) by A6, A7, A55, A56, FUNCT_1: 49;



 A62: ((x1 + ( (#) y1)) . t) = ((x1 . t) + (( (#) y1) . t)) by A57, VALUED_1:def 1

 .= ((x1 . t) + ( * (y1 . t))) by VALUED_1: 6;



 A63: ((x + ( (#) y)) . t) = ((x . t) + (( (#) y) . t)) by A58, VALUED_1:def 1

 .= ((x . t) + ( * (y . t))) by VALUED_1: 6;



 thus ((x | [.a, d.]) . x0) = (x . x0) by A55, FUNCT_1: 47

 .= (x1 . x0) by A59, A60, A61, A62, A63, COMPLEX1: 77

 .= ((x1 | [.a, d.]) . x0) by A56, A55, FUNCT_1: 49;

 end;

 hence thesis by A54, FUNCT_1: 2;

 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 be object st x0 in ( dom (y | [.a, d.])) holds ((y | [.a, d.]) . x0) = ((y1 | [.a, d.]) . x0)

 proof

 let x0 be object such that

 A66: x0 in ( dom (y | [.a, d.]));



 A67: ( dom (y | [.a, d.])) = (( dom y) /\ [.a, d.]) by RELAT_1: 61

 .= [.a, d.] by A3, A4, A51, XBOOLE_1: 1, XBOOLE_1: 28;

 [.a, d.] c= (( dom x1) /\ ( dom y1)) by A6, A7, XBOOLE_1: 19;

 then x0 in (( dom x1) /\ ( dom y1)) by A66, A67;

 then x0 in (( dom x1) /\ ( dom ( (#) y1))) by VALUED_1:def 5;

 then

 A68: x0 in ( dom (x1 + ( (#) y1))) by VALUED_1:def 1;

 [.a, d.] c= (( dom x) /\ ( dom y)) by A52, XBOOLE_1: 19;

 then x0 in (( dom x) /\ ( dom y)) by A66, A67;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by VALUED_1:def 5;

 then

 A69: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;

 reconsider t = x0 as Element of REAL by A66;



 A70: (C . t) = (C1 . t) by A1, A66, A67;



 A71: (C . t) = ((x + ( (#) y)) . t) by A3, A4, A51, A66, A67, FUNCT_1: 49;



 A72: (C1 . t) = ((x1 + ( (#) y1)) . t) by A6, A7, A66, A67, FUNCT_1: 49;



 A73: ((x1 + ( (#) y1)) . t) = ((x1 . t) + (( (#) y1) . t)) by A68, VALUED_1:def 1

 .= ((x1 . t) + ( * (y1 . t))) by VALUED_1: 6;



 A74: ((x + ( (#) y)) . t) = ((x . t) + (( (#) y) . t)) by A69, VALUED_1:def 1

 .= ((x . t) + ( * (y . t))) by VALUED_1: 6;



 thus ((y | [.a, d.]) . x0) = (y . x0) by A66, FUNCT_1: 47

 .= (y1 . x0) by A70, A71, A72, A73, A74, COMPLEX1: 77

 .= ((y1 | [.a, d.]) . x0) by A67, A66, FUNCT_1: 49;

 end;

 hence thesis by A65, FUNCT_1: 2;

 end;



 A75: [.a, d.] c= Z by A3, A4, A51;

 then

 A76: [.a, d.] c= Z3 by A6, A7, XBOOLE_1: 19;



 A77: ( rng ((x + ( (#) y)) | [.a, d.])) c= ( dom f)

 proof

 let y0 be object such that

 A78: y0 in ( rng ((x + ( (#) y)) | [.a, d.]));

 consider x0 be object such that

 A79: x0 in ( dom ((x + ( (#) y)) | [.a, d.])) & y0 = (((x + ( (#) y)) | [.a, d.]) . x0) by A78, FUNCT_1:def 3;



 A80: x0 in (( dom (x + ( (#) y))) /\ [.a, d.]) by A79, RELAT_1: 61;

 (( dom (x + ( (#) y))) /\ [.a, d.]) c= (( dom (x + ( (#) y))) /\ [.a, b.]) by A2, XBOOLE_1: 26, XXREAL_1: 34;

 then x0 in (( dom (x + ( (#) y))) /\ [.a, b.]) by A80;

 then

 A81: x0 in ( dom ((x + ( (#) y)) | [.a, b.])) by RELAT_1: 61;

 then

 A82: (((x + ( (#) y)) | [.a, b.]) . x0) in ( rng ((x + ( (#) y)) | [.a, b.])) by FUNCT_1: 3;

 (((x + ( (#) y)) | [.a, d.]) . x0) = ((x + ( (#) y)) . x0) by A79, FUNCT_1: 47

 .= (((x + ( (#) y)) | [.a, b.]) . x0) by A81, FUNCT_1: 47;

 hence thesis by A1, A3, A79, A82;

 end;



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

 proof

 let y0 be object such that

 A84: y0 in ( rng ((x1 + ( (#) y1)) | [.a, d.]));

 consider x0 be object such that

 A85: x0 in ( dom ((x1 + ( (#) y1)) | [.a, d.])) & y0 = (((x1 + ( (#) y1)) | [.a, d.]) . x0) by A84, FUNCT_1:def 3;

 x0 in (( dom (x1 + ( (#) y1))) /\ [.a, d.]) by A85, RELAT_1: 61;

 then

 A86: x0 in [.a, d.] by XBOOLE_0:def 4;

 then x0 in [.a, b.] by A51;

 then x0 in (( dom x) /\ ( dom y)) by A3, A4, XBOOLE_0:def 4;

 then x0 in ((( dom x) /\ ( dom y)) /\ [.a, b.]) by A51, A86, XBOOLE_0:def 4;

 then x0 in ((( dom x) /\ ( dom ( (#) y))) /\ [.a, b.]) by VALUED_1:def 5;

 then x0 in (( dom (x + ( (#) y))) /\ [.a, b.]) by VALUED_1:def 1;

 then x0 in ( dom ((x + ( (#) y)) | [.a, b.])) by RELAT_1: 61;

 then

 A87: (((x + ( (#) y)) | [.a, b.]) . x0) in ( rng ((x + ( (#) y)) | [.a, b.])) by FUNCT_1: 3;

 reconsider t = x0 as Element of REAL by A85;



 A88: (C . t) = ((x + ( (#) y)) . t) by A3, A4, A51, A86, FUNCT_1: 49;



 A89: (C1 . t) = ((x1 + ( (#) y1)) . t) by A6, A7, A86, FUNCT_1: 49;

 (((x1 + ( (#) y1)) | [.a, d.]) . x0) = ((x1 + ( (#) y1)) . x0) by A85, FUNCT_1: 47

 .= ((x + ( (#) y)) . x0) by A1, A86, A88, A89

 .= (((x + ( (#) y)) | [.a, b.]) . x0) by A51, A86, FUNCT_1: 49;

 hence thesis by A1, A3, A85, A87;

 end;



 A90: x is_differentiable_on Z3 & y is_differentiable_on Z3 by A3, A50, FDIFF_1: 26, XBOOLE_1: 17;



 A91: x1 is_differentiable_on Z3 & y1 is_differentiable_on Z3 by A6, A50, FDIFF_1: 26, XBOOLE_1: 17;



 A92: [.a, d.] c= ( dom x) & [.a, d.] c= ( dom y) by A3, A4, A51;



 hence ( integral (f,x,y,a,d,Z)) = ( integral (f,x,y,a,d,Z3)) by A3, A6, A7, A50, A77, A76, Lm1, XBOOLE_1: 17

 .= ( integral (f,x1,y1,a,d,Z3)) by A6, A7, A50, A53, A64, A75, A77, A83, A90, A91, A92, Lm2, XBOOLE_1: 19

 .= ( integral (f,x1,y1,a,d,Z1)) by A6, A7, A50, A76, A83, Lm1, XBOOLE_1: 17;

 end;



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

 proof

 reconsider Z3 = (Z /\ Z2) as Subset of REAL ;

 reconsider ZZ = Z, ZZ1 = Z2 as Subset of R^1 by TOPMETR: 17;

 ZZ is open & ZZ1 is open by A3, A12, BORSUK_5: 39;

 then (ZZ /\ ZZ1) is open by TOPS_1: 11;

 then

 A94: Z3 is open by BORSUK_5: 39;



 A95: [.d, b.] c= [.a, b.] by A2, XXREAL_1: 34;

 then

 A96: [.d, b.] c= ( dom x) & [.d, b.] c= ( dom y) by A3, A4;



 A97: (x | [.d, b.]) = (x2 | [.d, b.])

 proof



 A98: ( dom (x | [.d, b.])) = (( dom x) /\ [.d, b.]) by RELAT_1: 61

 .= [.d, b.] by A3, A4, A95, XBOOLE_1: 1, XBOOLE_1: 28

 .= (( dom x2) /\ [.d, b.]) by A12, A13, XBOOLE_1: 28

 .= ( dom (x2 | [.d, b.])) by RELAT_1: 61;

 for x0 be object st x0 in ( dom (x | [.d, b.])) holds ((x | [.d, b.]) . x0) = ((x2 | [.d, b.]) . x0)

 proof

 let x0 be object such that

 A99: x0 in ( dom (x | [.d, b.]));



 A100: ( dom (x | [.d, b.])) = (( dom x) /\ [.d, b.]) by RELAT_1: 61

 .= [.d, b.] by A3, A4, A95, XBOOLE_1: 1, XBOOLE_1: 28;

 [.d, b.] c= (( dom x2) /\ ( dom y2)) by A12, A13, XBOOLE_1: 19;

 then x0 in (( dom x2) /\ ( dom y2)) by A99, A100;

 then x0 in (( dom x2) /\ ( dom ( (#) y2))) by VALUED_1:def 5;

 then

 A101: x0 in ( dom (x2 + ( (#) y2))) by VALUED_1:def 1;

 [.d, b.] c= (( dom x) /\ ( dom y)) by A96, XBOOLE_1: 19;

 then x0 in (( dom x) /\ ( dom y)) by A99, A100;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by VALUED_1:def 5;

 then

 A102: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;

 reconsider t = x0 as Element of REAL by A99;



 A103: (C . t) = (C2 . t) by A1, A99, A100;



 A104: (C . t) = ((x + ( (#) y)) . t) by A3, A4, A95, A99, A100, FUNCT_1: 49;



 A105: (C2 . t) = ((x2 + ( (#) y2)) . t) by A12, A13, A99, A100, FUNCT_1: 49;



 A106: ((x2 + ( (#) y2)) . t) = ((x2 . t) + (( (#) y2) . t)) by A101, VALUED_1:def 1

 .= ((x2 . t) + ( * (y2 . t))) by VALUED_1: 6;



 A107: ((x + ( (#) y)) . t) = ((x . t) + (( (#) y) . t)) by A102, VALUED_1:def 1

 .= ((x . t) + ( * (y . t))) by VALUED_1: 6;



 thus ((x | [.d, b.]) . x0) = (x . x0) by A99, FUNCT_1: 47

 .= (x2 . x0) by A103, A104, A105, A106, A107, COMPLEX1: 77

 .= ((x2 | [.d, b.]) . x0) by A99, A100, FUNCT_1: 49;

 end;

 hence thesis by A98, FUNCT_1: 2;

 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 be object st x0 in ( dom (y | [.d, b.])) holds ((y | [.d, b.]) . x0) = ((y2 | [.d, b.]) . x0)

 proof

 let x0 be object such that

 A110: x0 in ( dom (y | [.d, b.]));



 A111: ( dom (y | [.d, b.])) = (( dom y) /\ [.d, b.]) by RELAT_1: 61

 .= [.d, b.] by A3, A4, A95, XBOOLE_1: 1, XBOOLE_1: 28;

 [.d, b.] c= (( dom x2) /\ ( dom y2)) by A12, A13, XBOOLE_1: 19;

 then x0 in (( dom x2) /\ ( dom y2)) by A110, A111;

 then x0 in (( dom x2) /\ ( dom ( (#) y2))) by VALUED_1:def 5;

 then

 A112: x0 in ( dom (x2 + ( (#) y2))) by VALUED_1:def 1;

 [.d, b.] c= (( dom x) /\ ( dom y)) by A96, XBOOLE_1: 19;

 then x0 in (( dom x) /\ ( dom y)) by A110, A111;

 then x0 in (( dom x) /\ ( dom ( (#) y))) by VALUED_1:def 5;

 then

 A113: x0 in ( dom (x + ( (#) y))) by VALUED_1:def 1;

 reconsider t = x0 as Element of REAL by A110;



 A114: (C . t) = (C2 . t) by A1, A110, A111;



 A115: (C . t) = ((x + ( (#) y)) . t) by A3, A4, A95, A110, A111, FUNCT_1: 49;



 A116: (C2 . t) = ((x2 + ( (#) y2)) . t) by A12, A13, A110, A111, FUNCT_1: 49;



 A117: ((x2 + ( (#) y2)) . t) = ((x2 . t) + (( (#) y2) . t)) by A112, VALUED_1:def 1

 .= ((x2 . t) + ( * (y2 . t))) by VALUED_1: 6;



 A118: ((x + ( (#) y)) . t) = ((x . t) + (( (#) y) . t)) by A113, VALUED_1:def 1

 .= ((x . t) + ( * (y . t))) by VALUED_1: 6;



 thus ((y | [.d, b.]) . x0) = (y . x0) by A110, FUNCT_1: 47

 .= (y2 . x0) by A114, A115, A116, A117, A118, COMPLEX1: 77

 .= ((y2 | [.d, b.]) . x0) by A111, A110, FUNCT_1: 49;

 end;

 hence thesis by A109, FUNCT_1: 2;

 end;



 A119: [.d, b.] c= Z by A3, A4, A95;

 then

 A120: [.d, b.] c= Z3 by A12, A13, XBOOLE_1: 19;



 A121: ( rng ((x + ( (#) y)) | [.d, b.])) c= ( dom f)

 proof

 let y0 be object such that

 A122: y0 in ( rng ((x + ( (#) y)) | [.d, b.]));

 consider x0 be object such that

 A123: x0 in ( dom ((x + ( (#) y)) | [.d, b.])) & y0 = (((x + ( (#) y)) | [.d, b.]) . x0) by A122, FUNCT_1:def 3;



 A124: x0 in (( dom (x + ( (#) y))) /\ [.d, b.]) by A123, RELAT_1: 61;

 (( dom (x + ( (#) y))) /\ [.d, b.]) c= (( dom (x + ( (#) y))) /\ [.a, b.]) by A2, XBOOLE_1: 26, XXREAL_1: 34;

 then x0 in (( dom (x + ( (#) y))) /\ [.a, b.]) by A124;

 then

 A125: x0 in ( dom ((x + ( (#) y)) | [.a, b.])) by RELAT_1: 61;

 then

 A126: (((x + ( (#) y)) | [.a, b.]) . x0) in ( rng ((x + ( (#) y)) | [.a, b.])) by FUNCT_1: 3;

 (((x + ( (#) y)) | [.d, b.]) . x0) = ((x + ( (#) y)) . x0) by A123, FUNCT_1: 47

 .= (((x + ( (#) y)) | [.a, b.]) . x0) by A125, FUNCT_1: 47;

 hence thesis by A1, A3, A123, A126;

 end;



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

 proof

 let y0 be object such that

 A128: y0 in ( rng ((x2 + ( (#) y2)) | [.d, b.]));

 consider x0 be object such that

 A129: x0 in ( dom ((x2 + ( (#) y2)) | [.d, b.])) & y0 = (((x2 + ( (#) y2)) | [.d, b.]) . x0) by A128, FUNCT_1:def 3;

 x0 in (( dom (x2 + ( (#) y2))) /\ [.d, b.]) by A129, RELAT_1: 61;

 then

 A130: x0 in [.d, b.] by XBOOLE_0:def 4;

 then x0 in [.a, b.] by A95;

 then x0 in (( dom x) /\ ( dom y)) by A3, A4, XBOOLE_0:def 4;

 then x0 in ((( dom x) /\ ( dom y)) /\ [.a, b.]) by A95, A130, XBOOLE_0:def 4;

 then x0 in ((( dom x) /\ ( dom ( (#) y))) /\ [.a, b.]) by VALUED_1:def 5;

 then x0 in (( dom (x + ( (#) y))) /\ [.a, b.]) by VALUED_1:def 1;

 then x0 in ( dom ((x + ( (#) y)) | [.a, b.])) by RELAT_1: 61;

 then

 A131: (((x + ( (#) y)) | [.a, b.]) . x0) in ( rng ((x + ( (#) y)) | [.a, b.])) by FUNCT_1: 3;

 reconsider t = x0 as Element of REAL by A129;



 A132: (C . t) = ((x + ( (#) y)) . t) by A3, A4, A95, A130, FUNCT_1: 49;



 A133: (C2 . t) = ((x2 + ( (#) y2)) . t) by A12, A13, A130, FUNCT_1: 49;

 (((x2 + ( (#) y2)) | [.d, b.]) . x0) = ((x2 + ( (#) y2)) . x0) by A129, FUNCT_1: 47

 .= ((x + ( (#) y)) . x0) by A1, A130, A132, A133

 .= (((x + ( (#) y)) | [.a, b.]) . x0) by A95, A130, FUNCT_1: 49;

 hence thesis by A1, A3, A129, A131;

 end;



 A134: x is_differentiable_on Z3 & y is_differentiable_on Z3 by A3, A94, FDIFF_1: 26, XBOOLE_1: 17;



 A135: x2 is_differentiable_on Z3 & y2 is_differentiable_on Z3 by A12, A94, FDIFF_1: 26, XBOOLE_1: 17;



 A136: [.d, b.] c= ( dom x) & [.d, b.] c= ( dom y) by A3, A4, A95;



 hence ( integral (f,x,y,d,b,Z)) = ( integral (f,x,y,d,b,Z3)) by A3, A12, A13, A94, A120, A121, Lm1, XBOOLE_1: 17

 .= ( integral (f,x2,y2,d,b,Z3)) by Lm2, A12, A13, A94, A97, A108, A119, A121, A127, A134, A135, A136, XBOOLE_1: 19

 .= ( integral (f,x2,y2,d,b,Z2)) by A12, A13, A94, A120, A127, Lm1, XBOOLE_1: 17;

 end;



 thus ( integral (f,C)) = (( integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + (( integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * )) by A1, A3, A5, Def4

 .= ((( integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + ( integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b))) + (( integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * )) by A1, A18, A39, A40, A41, INTEGRA6: 17

 .= ((( integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,d)) + ( integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),d,b))) + ((( integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,d)) + ( integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),d,b))) * )) by A1, A18, A39, A40, A44, INTEGRA6: 17

 .= (( integral (f,x1,y1,a,d,Z1)) + ( integral (f,x,y,d,b,Z))) by A49, A48, A47

 .= (( integral (f,C1)) + ( integral (f,C2))) by A6, A7, A8, A17, Def4, A93;

 end;