:: Complex Integral
::  by Masahiko Yamazaki , Hiroshi Yamazaki , Katsumi Wasaki and Yasunari Shidama
:: 
:: Received October 10, 2009
:: Copyright (c) 2009 Association of Mizar Users

environ

 vocabularies NUMBERS, SUBSET_1, FDIFF_1, SEQ_1, FUNCT_1, XREAL_0, ORDINAL1,
      ZFMISC_1, MCART_1, ARYTM_3, RELAT_1, XCMPLX_0, REAL_1, PARTFUN1,
      INTEGRA1, CFUNCT_1, COMPLEX1, VALUED_1, ARYTM_1, XBOOLE_0, TARSKI,
      XXREAL_0, XXREAL_1, RCOMP_1, ORDINAL2, SIN_COS, CARD_1, FDIFF_3, FUNCT_2,
      SEQ_2, TOPMETR, INTEGRA5, VFUNCT_1, XXREAL_2, INTEGR1C;
 notations TARSKI, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1,
      REAL_1, BINOP_1, RCOMP_1, FUNCT_3, SEQ_1, SEQ_2, FCONT_1, FDIFF_1,
      TOPMETR, MCART_1, INTEGRA1, INTEGRA5, SIN_COS, CFUNCT_1, VALUED_1,
      MESFUN6C, PRE_TOPC, FDIFF_3, STRUCT_0, XXREAL_2;
 constructors REAL_1, FDIFF_1, RFUNCT_3, FCONT_1, BINOP_2, INTEGRA5, RSSPACE,
      SIN_COS, TOPMETR, FDIFF_3, SEQ_1, MESFUN6C, SEQ_2;
 registrations XREAL_0, INTEGRA1, FUNCT_2, NUMBERS, ORDINAL1, MEMBERED,
      SIN_COS, FDIFF_1, SUBSET_1, XCMPLX_0, RELAT_1, XXREAL_0, XBOOLE_0,
      VALUED_0, VALUED_1;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
 definitions INTEGRA5, VALUED_1;
 theorems ZFMISC_1, XCMPLX_0, TOPMETR, SEQ_4, INTEGRA1, RFUNCT_1, FUNCT_1,
      SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, COMPLEX1, FUNCT_3, TARSKI, RCOMP_1,
      FCONT_1, RFUNCT_2, FDIFF_2, RELAT_1, XXREAL_1, FUNCT_2, NUMBERS,
      XBOOLE_0, XBOOLE_1, XREAL_1, INTEGRA5, SIN_COS, INTEGRA6, CFUNCT_1,
      VALUED_1, MESFUN6C, TOPS_1, FDIFF_3, RELSET_1, XXREAL_2, MCART_1,
      BORSUK_5;
 schemes FUNCT_2, FUNCT_7;

begin :: The Definition of Complex Curve and Complex Integral

reserve n,n1,m for Element of NAT;
reserve r,t,x1 for Element of REAL;
reserve h for convergent_to_0 Real_Sequence;
reserve c1 for constant Real_Sequence;
reserve p1 for real number;

definition
  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*<i>;
  existence
    proof
      deffunc F(Element of REAL,Element of REAL)
      = $1+$2*<i>;
A1: for x being Element of REAL, y being Element of REAL
    holds
    F(x,y) in COMPLEX by XCMPLX_0:def 2;
    consider
    f being Function of [:REAL,REAL:],COMPLEX such that
A2: for x,y being Element of REAL
    holds f.(x,y) = F(x,y) from FUNCT_7:sch 1(A1);
    deffunc G(Element of [:REAL,REAL:]) = f.($1`1,$1`2);
A3: now let p being 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*<i> by A2,A4;
      hence G(p) in COMPLEX by XCMPLX_0:def 2;
    end;
    consider g being Function of [:REAL,REAL:], COMPLEX such that
A5: for p being 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*<i>
      proof
        let p be Element of [:REAL,REAL:],
        a,b be Element of REAL such that
A6:     a = p`1 & b = p`2;
A7:     [a,b]`1 is Element of REAL by MCART_1:7;
        [a,b]`2 is Element of REAL by MCART_1:7; then
A8:     [a,b] is Element of [:REAL,REAL:] by A7,MCART_1:11;
A9:     [a,b]`1 = p`1 by A6,MCART_1:7;
        [a,b]`2 = p`2 by A6,MCART_1:7;then
        g.([a,b]) = f.(a,b) by A6,A5,A8,A9
        .= a+b*<i> 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*<i>;
    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*<i>;
    for p0 be set st p0 in [:REAL,REAL:] holds f.p0 = g.p0
      proof
        let p0 be set;
        assume
A12:    p0 in [:REAL,REAL:];then
        consider x0,y0 be set such that
A13:    x0 in REAL & y0 in REAL & p0 = [x0,y0] by ZFMISC_1:def 2;
        reconsider a = x0,b = y0 as Element of REAL by A13;
A14:    p0`1 = a by A13,MCART_1:7;
A15:    p0`2 = b by A13,MCART_1:7;
        f.p0 = a+b*<i> by A12,A10,A14,A15,A13
        .= g.p0 by A13,A12,A11,A14,A15;
        hence thesis;
      end;
    hence f = g by FUNCT_2:18;
  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;
  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 )*<i>;
  existence
    proof
A1:   dom <:x,y:> = dom x /\ dom y by FUNCT_3:def 8;
      rng <:x,y:> c= [:rng x,rng y:] by FUNCT_3:71;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:11;
      (Re f)* (R2-to-C) *xy is PartFunc of REAL,REAL;then
      reconsider u0=(Re f)* (R2-to-C) *<:x,y:> as PartFunc of REAL,REAL;
      (Im f)* (R2-to-C) *xy is PartFunc of REAL,REAL;
      then
      reconsider v0=(Im f)* (R2-to-C) *<:x,y:> as PartFunc of REAL,REAL;
      integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
      + integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i>
      is Complex by XCMPLX_0:def 2;
      hence thesis;
    end;
  uniqueness;
end;

definition
  let C be PartFunc of REAL,COMPLEX;
  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+<i>(#)y) | [.a,b.];
end;

registration
  cluster C1-curve-like 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
A4:   C = (x+<i>(#)y) | [.a,b.];
      take C;
A5:   dom (x+<i>(#)y) = REAL by FUNCT_2:def 1;
      dom C = dom (x+<i>(#)y) /\ [.a,b.] by A4,RELAT_1:90;then
A6:   [.a,b.] = dom C by A5,XBOOLE_1:28;
A7:   Z is open by RCOMP_1:25;
A8:   [.a,b.] c= Z by XXREAL_1:47;
A9:   x is_differentiable_on Z by A7,FDIFF_1:34,SIN_COS:72;
A10:  y is_differentiable_on Z by A7,FDIFF_1:34,SIN_COS:73;
A11:  sin = sin|(REAL)
        proof
A12:      dom (sin|(REAL)) = dom (sin) /\ (REAL) by RELAT_1:90
          .= REAL by SIN_COS:27;
          for x0 be set st x0 in dom sin holds sin.x0 = sin|(REAL).x0
          by FUNCT_1:72;
          hence thesis by A12,SIN_COS:27,FUNCT_1:9;
        end;
      sin|Z is continuous by A11,FCONT_1:17;then
      (-sin)|Z is continuous by SIN_COS:27,FCONT_1:22;then
A13:  -sin|Z is continuous by RFUNCT_1:62;
A14:  dom(-sin|Z) = dom((-sin)|Z) by RFUNCT_1:62
      .= dom(-sin) /\ Z by RELAT_1:90
      .= REAL /\ Z by SIN_COS:27,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
A15:      x1 in Z;
A16:      (-sin|Z).x1 = ((-sin)|Z).x1 by RFUNCT_1:62
          .= (-sin).x1 by A15,FUNCT_1:72
          .= -(sin.x1) by RFUNCT_1:74
          .= -sin|Z.x1 by A15,FUNCT_1:72;
          diff(x,x1) = -sin.x1 by SIN_COS:72
          .= (-sin|Z).x1 by A16,A15,FUNCT_1:72;
          hence thesis;
        end; then
A17:  x`|Z is continuous by A9,A13,A14,FDIFF_1:def 8;
A18:  cos = cos|(REAL)
      proof
A19:    dom (cos|(REAL)) = dom (cos) /\ (REAL) by RELAT_1:90
        .= REAL by SIN_COS:27;
        for x0 be set st x0 in dom cos holds cos.x0 = cos|(REAL).x0
        by FUNCT_1:72;
        hence thesis by A19,SIN_COS:27,FUNCT_1:9;
      end;
A20:  cos|Z is continuous by A18,FCONT_1:17;
A21:  dom(cos|Z) = dom(cos) /\ Z by RELAT_1:90
      .= Z by XBOOLE_1:28,SIN_COS:27;
      for x1 st x1 in Z holds (cos|Z).x1 = diff(y,x1)
      proof
        let x1 such that
A22:    x1 in Z;
        diff(y,x1) = cos.x1 by SIN_COS:73
          .= (cos|Z).x1 by A22,FUNCT_1:72;
        hence thesis;
      end;
    then y`|Z is continuous by A10,A20,A21,FDIFF_1:def 8;
    hence thesis by A4,A6,A7,A8,A9,A10,A17,Def3,SIN_COS:27;
  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 + <i>(#)y) | [.a,b.] ) c= dom f
holds
integral(f,x,y,a,b,Z1) = integral(f,x,y,a,b,Z2)
proof
  let a,b be Real,
  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 + <i>(#)y) | [.a,b.] ) c=dom f;
A2: x is_differentiable_on Z1 &
  y is_differentiable_on Z1 by A1,FDIFF_1:34;
  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 )*<i> 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 )*<i> by Def2;
  reconsider AB=[.a,b.] as closed-interval Subset of REAL
  by A1,INTEGRA1:def 1;
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 8
      .= (dom u01 /\ Z1) /\ ( dom v01 /\ Z1) by A2,FDIFF_1:def 8
      .= 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 8
      .= (dom u02 /\ Z2) /\ ( dom v02 /\ Z2) by A1,FDIFF_1:def 8
      .= 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:90
      .= (dom u01 /\ dom v01) /\ (Z1 /\ AB) by XBOOLE_1:16,A6
      .= (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:90
      .= (dom u01 /\ dom v01) /\ (Z2 /\ AB) by XBOOLE_1:16,A7
      .= (dom u01 /\ dom v01) /\ AB by A1,XBOOLE_1:28,XBOOLE_1:1;
      for x0 being set st x0 in dom((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB )
      holds
      ((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB).x0
      = ((u02(#)(x`|Z2) - v02(#)(y`|Z2)) | AB ).x0
        proof
          let x0 being set 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:90;
          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 8;
          reconsider x0 as Real by A10;
A14:      ((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB).x0
          = (u01(#)(x`|Z1) - v01(#)(y`|Z1)).x0 by A10,FUNCT_1:70
          .= (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 8;
          x0 in dom(u02(#)(x`|Z2) - v02(#)(y`|Z2)) /\ AB
          by A8,A9,A10,RELAT_1:90;
          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 8;
          ((u02(#)(x`|Z2) - v02(#)(y`|Z2)) | AB ).x0
          = (u02(#)(x`|Z2) - v02(#)(y`|Z2)).x0 by A8,A9,A10,FUNCT_1:70
          .= (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 8; 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 8;
          hence thesis by A2,A13,A14,FDIFF_1:def 8;
        end;
      hence thesis by A8,A9,FUNCT_1:def 17;
    end;
A19: 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;
A20: (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
A21:  dom(v01(#)(x`|Z1) + u01(#)(y`|Z1))
      = (dom v01 /\ Z1) /\ ( dom u01 /\ dom(y`|Z1)) by A2,FDIFF_1:def 8
      .= (dom v01 /\ Z1) /\ ( dom u01 /\ Z1) by A2,FDIFF_1:def 8
      .= 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
A22:  dom(v02(#)(x`|Z2) + u02(#)(y`|Z2))
      = (dom v02 /\ Z2) /\ ( dom u02 /\ dom(y`|Z2)) by A1,FDIFF_1:def 8
      .= (dom v02 /\ Z2) /\ ( dom u02 /\ Z2) by A1,FDIFF_1:def 8
      .= 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;
A23:  dom((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB)
      = dom (v01(#)(x`|Z1) + u01(#)(y`|Z1)) /\ AB by RELAT_1:90
      .= (dom v01 /\ dom u01) /\ (Z1 /\ AB) by XBOOLE_1:16,A21
      .= (dom v01 /\ dom u01) /\ AB by A1,XBOOLE_1:28;
A24:  dom((v02(#)(x`|Z2) + u02(#)(y`|Z2)) | AB)
      = dom (v02(#)(x`|Z2) + u02(#)(y`|Z2)) /\ AB by RELAT_1:90
      .= (dom v01 /\ dom u01) /\ (Z2 /\ AB) by XBOOLE_1:16,A22
      .= (dom v01 /\ dom u01) /\ AB by A1,XBOOLE_1:1,XBOOLE_1:28;
      for x0 being set st x0 in dom((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB )
      holds
      ((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB).x0
      = ((v02(#)(x`|Z2) + u02(#)(y`|Z2)) | AB).x0
        proof
          let x0 being set such that
A25:      x0 in dom((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB );
          x0 in dom(v01(#)(x`|Z1) + u01(#)(y`|Z1)) /\ AB by A25,RELAT_1:90;
          then
A26:      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
A27:      x0 in dom(v01(#)(x`|Z1)) & x0 in dom(u01(#)(y`|Z1))
          by XBOOLE_0:def 4;then
          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 8;
          reconsider x0 as Real by A25;
          ((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB).x0
          = (v01(#)(x`|Z1) + u01(#)(y`|Z1)).x0 by A25,FUNCT_1:70
          .= (v01(#)(x`|Z1)).x0 + (u01(#)(y`|Z1)).x0 by A26,VALUED_1:def 1
          .= v01.x0*(x`|Z1).x0 + (u01(#)(y`|Z1)).x0 by A27,VALUED_1:def 4
          .= v01.x0*(x`|Z1).x0 + u01.x0*(y`|Z1).x0 by A27,VALUED_1:def 4
          .= v01.x0*diff(x,x0) + u01.x0*(y`|Z1).x0
          by A2,A28,FDIFF_1:def 8; 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 8;
          x0 in dom(v02(#)(x`|Z2) + u02(#)(y`|Z2)) /\ AB
          by A23,A24,A25,RELAT_1:90; 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 8;
          ((v02(#)(x`|Z2) + u02(#)(y`|Z2)) | AB ).x0
          = (v02(#)(x`|Z2) + u02(#)(y`|Z2)).x0 by A23,A24,A25,FUNCT_1:70
          .= (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 8;
          hence thesis by A1,A3,A4,A29,A32,FDIFF_1:def 8;
        end;
      hence thesis by A23,A24,FUNCT_1:def 17;
    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 A20
  .=integral( v02(#)(x`|Z2) + u02(#)(y`|Z2) ,a,b) by INTEGRA5:19;
  hence thesis by A3,A4,A19;
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 + <i>(#)y1) | [.a,b.] ) c=dom f &
x2 is_differentiable_on Z & y2 is_differentiable_on Z &
rng ( (x2 + <i>(#)y2) | [.a,b.] ) c=dom f
holds
integral(f,x1,y1,a,b,Z) = integral(f,x2,y2,a,b,Z)
proof
  let a,b be Real,
  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 + <i>(#)y1) | [.a,b.] ) c= dom f &
  x2 is_differentiable_on Z & y2 is_differentiable_on Z &
  rng ( (x2 + <i>(#)y2) | [.a,b.] ) c=dom f;
  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 )*<i> 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 )*<i> by Def2;
  reconsider AB=[.a,b.] as closed-interval Subset of REAL
  by A1,INTEGRA1:def 1;
A4: now assume
A5: not (a = b or a < b);then
    0 < b - a or 0 < a - b by XREAL_1:57;then
    a < a + (b -a) or 0 < a - b by XREAL_1:31;then
    a < b or b < b + (a - b) by XREAL_1:31;
    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 set st x0 in dom(u01 | AB)
        holds
        x0 in dom(u02 | AB)
        proof
          let x0 be set such that
A10:      x0 in dom(u01 | AB);
          x0 in dom u01 /\ AB by A10,RELAT_1:90;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:21;then
          x0 in AB &
          [x1.x0,y1.x0] in dom((Re f)* (R2-to-C)) by FUNCT_3:def 8; then
          x0 in AB &
          [(x1 | AB).x0,y1.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:72;
          then
          x0 in AB &
          [(x2 | AB).x0,(y2 | AB).x0] in dom((Re f)* (R2-to-C))
          by A1,FUNCT_1:72;then
          x0 in AB & [(x2 | AB).x0,y2.x0] in dom((Re f)* (R2-to-C))
          by FUNCT_1:72; then
A12:      x0 in AB &
          [x2.x0,y2.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:72;
          x0 in dom x2 /\ dom y2 by A1,A11,XBOOLE_0:def 4;then
          x0 in dom <:x2,y2:> by FUNCT_3:def 8;then
          x0 in AB & x0 in dom <:x2,y2:>
          & <:x2,y2:>.x0 in dom((Re f)* (R2-to-C))
          by A12,FUNCT_3:def 8;then
          x0 in AB & x0 in dom u02 by A3,FUNCT_1:21;then
          x0 in dom u02 /\ AB by XBOOLE_0:def 4;
          hence thesis by RELAT_1:90;
        end;
        for x0 be set st x0 in dom(u02 | AB) holds x0 in dom(u01 | AB)
        proof
          let x0 be set such that
A13:      x0 in dom(u02 | AB);
          x0 in dom u02 /\ AB by A13,RELAT_1:90;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:21;then
          x0 in AB &
          [x2.x0,y2.x0] in dom((Re f)* (R2-to-C)) by FUNCT_3:def 8;
          then
          x0 in AB &
          [(x2 | AB).x0,y2.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:72;
          then
          x0 in AB &
          [(x1 | AB).x0,(y1 | AB).x0] in dom((Re f)* (R2-to-C))
          by A1,FUNCT_1:72;then
          x0 in AB & [(x1 | AB).x0,y1.x0] in dom((Re f)* (R2-to-C))
          by FUNCT_1:72;then
A15:      x0 in AB &
          [x1.x0,y1.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:72;
          x0 in dom x1 /\ dom y1 by A1,A14,XBOOLE_0:def 4;then
          x0 in dom <:x1,y1:> by FUNCT_3:def 8;then
          x0 in AB & x0 in dom <:x1,y1:> &
          <:x1,y1:>.x0 in dom((Re f)* (R2-to-C))
          by A15,FUNCT_3:def 8;then
          x0 in AB & x0 in dom u01 by A2,FUNCT_1:21;then
          x0 in dom u01 /\ AB by XBOOLE_0:def 4;
          hence thesis by RELAT_1:90;
        end;
        hence thesis by A9,TARSKI:2;
      end;
      for x0 be set st x0 in dom(u01 | AB) holds
      (u01 | AB).x0 = (u02 | AB).x0
      proof
        let x0 be set such that
A16:    x0 in dom(u01 | AB);
        x0 in dom u01 /\ AB by A16,RELAT_1:90;then
A17:    x0 in AB by XBOOLE_0:def 4;
        reconsider x0 as Real by A16;
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 8;then
A19:    u01.x0 = ((Re f)*(R2-to-C)).(<:x1,y1:>.x0) by A2,FUNCT_1:23;
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 8;then
        u02.x0 = ((Re f)*(R2-to-C)).(<:x2,y2:>.x0) by A3,FUNCT_1:23;
        then
A21:    u02.x0 = ((Re f)*(R2-to-C)).([x2.x0,y2.x0])
        by A17,A20,FUNCT_3:68;
A22:    x1.x0 = (x1| [.a,b.]).x0 by A17,FUNCT_1:72
        .= x2.x0 by A17,FUNCT_1:72,A1;
A23:    y1.x0 = (y1| [.a,b.]).x0 by A17,FUNCT_1:72
        .= y2.x0 by A17,FUNCT_1:72,A1;
        u01.x0 = (u01 | AB).x0 & u02.x0 = (u02 | AB).x0
        by A17,FUNCT_1:72;
        hence thesis by A17,A18,A19,A21,A22,A23,FUNCT_3:68;
      end;
      hence thesis by A8,FUNCT_1:def 17;
    end;
A24: (x1`|Z)| AB = (x2`|Z)| AB
    proof
A25:  dom ((x1`|Z)| AB) = dom (x1`|Z) /\ AB by RELAT_1:90
      .= Z /\ AB by A1,FDIFF_1:def 8
      .= AB by A1,XBOOLE_1:28;
A26:  dom ((x2`|Z)| AB) = dom (x2`|Z) /\ AB by RELAT_1:90
      .= Z /\ AB by A1,FDIFF_1:def 8
      .= AB by A1, XBOOLE_1:28;
      for x0 be set st x0 in dom((x1`|Z)| AB) holds
      ((x1`|Z)| AB).x0 = ((x2`|Z)| AB).x0
      proof
        let x0 be set such that
A27:    x0 in dom((x1`|Z)| AB);
        reconsider x0 as Real by A27;
A28:    ((x2`|Z)| AB).x0 = (x2`|Z).x0 by A25,A27,FUNCT_1:72;
A29:    (x1`|Z).x0 = diff(x1,x0) by A1,A25,A27,FDIFF_1:def 8;
A30:    (x2`|Z).x0 = diff(x2,x0) by A1,A25,A27,FDIFF_1:def 8;
A31:    now assume
A32:      not (x0 in ].a,b.[ or x0 = a or x0 = b);
          x0 in {r where r is 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:57;then
            a < a + (x0 -a) or 0 < a - x0 by XREAL_1:31;then
            a < x0 or x0 < x0 + (a - x0) by XREAL_1:31;
            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:57;then
            b < b + (x0 -b) or 0 < b - x0 by XREAL_1:31;then
            b < x0 or x0 < x0 + (b - x0) by XREAL_1:31;
            hence contradiction by A33,A37;
          end;
          not (x0 in {q where q is Real: a<q & q<b}) by A32,RCOMP_1:def 2;
          hence contradiction by A32,A34,A36;
        end;
        diff(x1,x0) = diff(x2,x0)
        proof
          per cases by A31;
          suppose
A39:        x0 = a;
            x0 in {r where r is Real: a <= r & r <= b} by A1,A39;then
A40:        x0 in [.a,b.] by RCOMP_1:def 1;then
A41:        x1 is_differentiable_in x0 by A1,FDIFF_1:16;then
A42:        x1 is_right_differentiable_in x0 &
            diff(x1,x0) = Rdiff(x1,x0) by FDIFF_3:22;
            x2 is_differentiable_in x0 by A1,A40,FDIFF_1:16;then
A43:        x2 is_right_differentiable_in x0 &
            diff(x2,x0) = Rdiff(x2,x0) by FDIFF_3:22;
A44:        x1 - x2 is_right_differentiable_in x0 by A42,A43,FDIFF_3:17;
            Rdiff(x1,x0) = Rdiff(x2,x0)
            proof
A45:          Rdiff(x1,x0) - Rdiff(x2,x0) = Rdiff(x1-x2,x0)
              by A42,A43,FDIFF_3:17;
              for h,c1 st rng c1 = {x0} & rng (h+c1) c= dom (x1-x2) &
              (for n holds h.n > 0) holds
              lim (h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)) = 0
              proof
                let h,c1 such that
A46:            rng c1 = {x0} & rng (h+c1) c= dom (x1-x2) &
                (for n holds h.n > 0);
A47:            h is convergent & lim h = 0 by FDIFF_1:def 1;
A48:            0 < b - x0 by A6,A39,XREAL_1:52;
                consider n such that
A49:            for m st n<=m holds abs(h.m - 0) < (b - x0)/2
                by A47,A48,SEQ_2:def 7;
A50:            for p1 st 0<p1 ex n1 st for m st n1 <= m
                holds
                abs((h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m-0) < p1
                proof
                  let p1 such that
A51:              0 < p1;
                  take n;
                  for m st n <= m holds
                  (h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m = 0
                  proof
                    let m such that
A52:                n <= m;
A53:                abs(h.m - 0) < (b - x0)/2 by A49,A52;
A54:                0 < h.m by A46;then
A55:                h.m < (b - x0)/2 by A53,ABSVALUE:def 1;
A56:                a + 0 <= x0 + h.m by A39,A54,XREAL_1:9;
                    x0 + h.m <= x0 + (b - x0)/2 by A55,XREAL_1:9;then
A57:                x0 + h.m + 0 <= b - (b - x0)/2 + (b - x0)/2
                    by A48,XREAL_1:9;
A58:                [.a,b.] c= dom x1 /\ dom x2 by A1,XBOOLE_1:19;then
                    x0 in dom x1 /\ dom x2 by A40;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 is 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 A46,TARSKI:def 1;
A63:                lim c1 = c1.m by SEQ_4:41;
A64:                (h+c1).m = h.m + c1.m by SEQ_1:11
                    .= h.m + x0 by A62,A63,SEQ_4:40;
A65:                rng c1 c= dom (x1-x2)
                    proof
                      for x be set st x in rng c1 holds
                      x in dom (x1-x2) by A46,A59,TARSKI:def 1;
                      hence thesis by TARSKI:def 3;
                    end;
A66:                (h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m
                    = (h").m*((x1-x2)/*(h+c1) - (x1-x2)/*c1).m by SEQ_1:12
                    .= (h").m*(((x1-x2)/*(h+c1)).m - ((x1-x2)/*c1).m )
                    by RFUNCT_2:6
                    .= (h").m*((x1-x2).((h+c1).m) - ((x1-x2)/*c1).m )
                    by A46,FUNCT_2:185
                    .= (h").m*((x1-x2).((h+c1).m) - (x1-x2).(c1.m) )
                    by A65,FUNCT_2:185
                    .= (h").m*((x1-x2).(h.m+x0) - (x1-x2).x0 )
                    by A62,A63,SEQ_4:40,A64;
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:72
                    .= (x1 | [.a,b.]).(h.m+x0) - (x2 | [.a,b.]).(h.m+x0)
                    by A61,FUNCT_1:72
                    .= 0 by A1;
                    (x1-x2).x0 = x1.x0 - x2.x0 by A59,VALUED_1:13
                    .= (x1 | [.a,b.]).x0 - x2.x0 by A40,FUNCT_1:72
                    .= (x1 | [.a,b.]).x0 - (x2 | [.a,b.]).x0
                    by A40,FUNCT_1:72
                    .= 0 by A1;
                    hence thesis by A66,A67;
                  end;
                  hence thesis by A51,COMPLEX1:130;
                end;
                (h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1))
                is convergent by A50,SEQ_2:def 6;
                hence thesis by A50,SEQ_2:def 7;
              end;then
              Rdiff(x1,x0) - Rdiff(x2,x0) = 0 by A44,A45,FDIFF_3:def 6;
              hence thesis;
            end;
            hence thesis by A41,A43,FDIFF_3:22;
          end;
          suppose
A68:        x0 in ].a,b.[;
A69:        ].a,b.[ is open by RCOMP_1:25;
A70:        ].a,b.[ c= [.a,b.]
            proof
              for x0 be set st x0 in ].a,b.[ holds x0 in [.a,b.]
              proof
                let x0 be set such that
A71:            x0 in ].a,b.[;
                x0 in {r where r is 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 is Real : a <= r & r <= b } by A72;
                hence thesis by RCOMP_1:def 1;
              end;
              hence thesis by TARSKI:def 3;
            end;then
A73:        x1 is_differentiable_on ].a,b.[
            by A1,A69,XBOOLE_1:1,FDIFF_1:34; 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 8;
A76:        x2 is_differentiable_on ].a,b.[
            by A69,A70,A1,XBOOLE_1:1,FDIFF_1:34;
            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 8;
A79:        dom (x1| (].a,b.[) )
            = dom x1 /\ (].a,b.[) by RELAT_1:90
            .= ].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:90;
            for x0 be set st x0 in dom (x1| (].a,b.[) ) holds
            (x1| (].a,b.[) ).x0 = (x2| (].a,b.[) ).x0
            proof
              let x0 be set such that
A80:          x0 in dom (x1| (].a,b.[) );
A81:          dom (x1| (].a,b.[) )
              = dom x1 /\ (].a,b.[) by RELAT_1:90
              .= ].a,b.[ by A1,A70,XBOOLE_1:1,XBOOLE_1:28;
              (x1| (].a,b.[) ).x0
              = x1.x0 by A80,A81,FUNCT_1:72
              .= (x1| ([.a,b.]) ).x0 by A70,A80,A81,FUNCT_1:72
              .= x2.x0 by A70,A80,A81,FUNCT_1:72,A1
              .=(x2| (].a,b.[) ).x0 by A80,A81,FUNCT_1:72;
              hence thesis;
            end;
            hence thesis by A74,A75,A77,A78,A79,FUNCT_1:9;
          end;
          suppose
A82:        x0 = b;
            x0 in {r where r is Real: a<=r & r<=b} by A1,A82;then
A83:        x0 in [.a,b.] by RCOMP_1:def 1;then
A84:        x1 is_differentiable_in x0 by A1,FDIFF_1:16;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:16;then
A86:        x2 is_left_differentiable_in x0 &
            diff(x2,x0) = Ldiff(x2,x0) by FDIFF_3:22;
A87:        x1 - x2 is_left_differentiable_in x0 by A85,A86,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 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 holds h.n < 0);
A90:            h is convergent & lim h = 0 by FDIFF_1:def 1;
A91:            0 < b - a by A6,XREAL_1:52;
                consider n such that
A92:            for m st n<=m holds abs(h.m - 0) < (x0 - a)/2
                by A82,A90,A91,SEQ_2:def 7;
A93:            for p1 st 0<p1 ex n1 st for m st n1 <= m
                holds
                abs((h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m-0) < p1
                proof
                  let p1 such that
A94:              0 < p1;
                  take n;
                  for m st n <= m holds
                  (h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m = 0
                  proof
                    let m such that
A95:                n <= m;
A96:                abs(h.m - 0) < (x0 - a)/2 by A92,A95;
A97:                h.m < 0 by A89;then
A98:                -h.m < (x0 - a)/2 by A96,ABSVALUE:def 1;
A99:                x0 + h.m <= b + 0 by A82,A97,XREAL_1:9;
                    x0 - (x0 - a)/2 <= x0 - (-h.m) by A98,XREAL_1:15;then
A100:               a + (x0 - a)/2 - (x0 - a)/2 <= x0 + h.m - 0
                    by A82,A91,XREAL_1:15;
A101:               [.a,b.] c= dom x1 /\ dom x2 by A1,XBOOLE_1:19;then
                    x0 in dom x1 /\ dom x2 by A83;then
A102:               x0 in dom(x1-x2) by VALUED_1:12;
A103:               [.a,b.] c= dom(x1-x2) by A101,VALUED_1:12;
                    x0 + h.m in {r where r is Real : a <= r & r <= b }
                    by A99,A100;then
A104:               x0 + h.m in [.a,b.] by RCOMP_1:def 1;
                    x0 in rng c1 by A89,TARSKI:def 1;then
A105:               lim c1 = x0 by SEQ_4:40;
A106:               (h+c1).m = h.m + c1.m by SEQ_1:11
                    .= h.m + x0 by A105,SEQ_4:41;
A107:               rng c1 c= dom (x1-x2)
                    proof
                      for x be set st x in rng c1 holds
                      x in dom (x1-x2) by A89,A102,TARSKI:def 1;
                      hence thesis by TARSKI:def 3;
                    end;
A108:               (h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m
                    = (h").m*((x1-x2)/*(h+c1) - (x1-x2)/*c1).m
                    by SEQ_1:12
                    .= (h").m*(((x1-x2)/*(h+c1)).m - ((x1-x2)/*c1).m )
                    by RFUNCT_2:6
                    .= (h").m*((x1-x2).((h+c1).m) - ((x1-x2)/*c1).m )
                    by A89,FUNCT_2:185
                    .= (h").m*((x1-x2).((h+c1).m) - (x1-x2).(c1.m) )
                    by A107,FUNCT_2:185
                    .= (h").m*((x1-x2).(h.m+x0) - (x1-x2).x0 )
                    by A105,SEQ_4:41,A106;
A109:               (x1-x2).(h.m+x0)
                    = x1.(h.m+x0) - x2.(h.m+x0) by A103,A104,VALUED_1:13
                    .= (x1 | [.a,b.]).(h.m+x0) - x2.(h.m+x0)
                    by A104,FUNCT_1:72
                    .= (x1 | [.a,b.]).(h.m+x0) - (x2 | [.a,b.]).(h.m+x0)
                    by A104,FUNCT_1:72
                    .= 0 by A1;
                    (x1-x2).x0 = x1.x0 - x2.x0 by A102,VALUED_1:13
                    .= (x1 | [.a,b.]).x0 -  x2.x0 by A83,FUNCT_1:72
                    .= (x1 | [.a,b.]).x0 -  (x2 | [.a,b.]).x0
                    by A83,FUNCT_1:72
                    .= 0 by A1;
                    hence thesis by A108,A109;
                  end;
                  hence thesis by A94,COMPLEX1:130;
                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 A25,A27,A28,A29,A30,FUNCT_1:72;
      end;
      hence thesis by A25,A26,FUNCT_1:def 17;
    end;
A110: v01 | AB = v02 | AB
    proof
A111: dom(v01 | AB) = dom(v02 | AB)
      proof
A112:   for x0 be set st x0 in dom(v01 | AB)
        holds
        x0 in dom(v02 | AB)
        proof
          let x0 be set such that
A113:     x0 in dom(v01 | AB);
          x0 in dom v01 /\ AB by A113,RELAT_1:90;then
A114:     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:21;then
          x0 in AB &
          [x1.x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_3:def 8;then
          x0 in AB &
          [(x1 | AB).x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:72;
          then
          x0 in AB &
          [(x2 | AB).x0,(y2 | AB).x0] in dom((Im f)* (R2-to-C))
          by A1,FUNCT_1:72;then
          x0 in AB &
          [(x2 | AB).x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:72;
          then
A115:     x0 in AB &
          [x2.x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:72;
          x0 in dom x2 /\ dom y2 by A1,A114,XBOOLE_0:def 4;then
          x0 in dom <:x2,y2:> by FUNCT_3:def 8;then
          x0 in AB & x0 in dom <:x2,y2:> &
          <:x2,y2:>.x0 in dom((Im f)* (R2-to-C))
          by A115,FUNCT_3:def 8;then
          x0 in AB & x0 in dom v02 by A3,FUNCT_1:21;then
          x0 in dom v02 /\ AB by XBOOLE_0:def 4;
          hence thesis by RELAT_1:90;
        end;
        for x0 be set st x0 in dom(v02 | AB) holds x0 in dom(v01 | AB)
        proof
          let x0 be set such that
A116:     x0 in dom(v02 | AB);
          x0 in dom v02 /\ AB by A116,RELAT_1:90;then
A117:     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:21;then
          x0 in AB &
          [x2.x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_3:def 8;then
          x0 in AB &
          [(x2 | AB).x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:72;
          then x0 in AB &
          [(x1 | AB).x0,(y1 | AB).x0] in dom((Im f)* (R2-to-C))
          by A1,FUNCT_1:72;then
          x0 in AB &
          [(x1 | AB).x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:72;
          then
A118:     x0 in AB &
          [x1.x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:72;
          x0 in dom x1 /\ dom y1 by A1,A117,XBOOLE_0:def 4;then
          x0 in dom <:x1,y1:> by FUNCT_3:def 8;then
          x0 in AB & x0 in dom <:x1,y1:> &
          <:x1,y1:>.x0 in dom((Im f)* (R2-to-C))
          by A118,FUNCT_3:def 8;then
          x0 in AB & x0 in dom v01 by A2,FUNCT_1:21;then
          x0 in dom v01 /\ AB by XBOOLE_0:def 4;
          hence thesis by RELAT_1:90;
        end;
        hence thesis by A112,TARSKI:2;
      end;
      for x0 be set st x0 in dom(v01 | AB)
      holds
      (v01 | AB).x0 = (v02 | AB).x0
      proof
        let x0 be set such that
A119:   x0 in dom(v01 | AB);
        x0 in dom v01 /\ AB by A119,RELAT_1:90;then
A120:   x0 in AB by XBOOLE_0:def 4;
        reconsider x0 as Real by A119;
A121:   AB c= dom x1 /\ dom y1 by A1,XBOOLE_1:19;then
        x0 in dom x1 /\ dom y1 by A120;then
        x0 in dom (<:x1,y1:>) by FUNCT_3:def 8;then
A122:   v01.x0 = ((Im f)*(R2-to-C)).(<:x1,y1:>.x0) by A2,FUNCT_1:23;
A123:   AB c= dom x2 /\ dom y2 by A1,XBOOLE_1:19;then
        x0 in dom x2 /\ dom y2 by A120;then
        x0 in dom (<:x2,y2:>) by FUNCT_3:def 8;then
        v02.x0 = ((Im f)*(R2-to-C)).(<:x2,y2:>.x0) by A3,FUNCT_1:23;then
A124:   v02.x0 = ((Im f)*(R2-to-C)).([x2.x0,y2.x0])
        by A120,A123,FUNCT_3:68;
A125:   x1.x0 = (x1| [.a,b.]).x0 by A120,FUNCT_1:72
        .= x2.x0 by A120, FUNCT_1:72,A1;
A126:   y1.x0 = (y1| [.a,b.]).x0 by A120,FUNCT_1:72
        .= y2.x0 by A120, FUNCT_1:72,A1;
        v01.x0 = (v01 | AB).x0 & v02.x0 = (v02 | AB).x0 by A120,FUNCT_1:72;
        hence thesis by A125,A126,A122,A120,A121,FUNCT_3:68,A124;
      end;
      hence thesis by A111,FUNCT_1:def 17;
    end;
A127: (y1`|Z)| AB = (y2`|Z)| AB
    proof
A128: dom ((y1`|Z)| AB)
      = dom (y1`|Z) /\ AB by RELAT_1:90
      .= Z /\ AB by A1,FDIFF_1:def 8
      .= AB by A1,XBOOLE_1:28;
A129: dom ((y2`|Z)| AB)
      = dom (y2`|Z) /\ AB by RELAT_1:90
      .= Z /\ AB by A1,FDIFF_1:def 8
      .= AB by A1,XBOOLE_1:28;
      for x0 be set st x0 in dom((y1`|Z)| AB)
      holds
      ((y1`|Z)| AB).x0 = ((y2`|Z)| AB).x0
      proof
        let x0 be set such that
A130:   x0 in dom((y1`|Z)| AB);
        reconsider x0 as Real by A130;
A131:   ((y2`|Z)| AB).x0 = (y2`|Z).x0 by A128,A130,FUNCT_1:72;
A132:   (y1`|Z).x0 = diff(y1,x0) by A1,A130,A128,FDIFF_1:def 8;
A133:   (y2`|Z).x0 = diff(y2,x0) by A1,A130,A128,FDIFF_1:def 8;
A134:   now assume
A135:     not (x0 in ].a,b.[ or x0 = a or x0 = b);
          x0 in {r where r is Real: a <= r & r <= b}
          by A128,A130,RCOMP_1:def 1;then
A136:     ex r be Real st r=x0 & a<=r & r<=b;
A137:     now assume
A138:       not (a = x0 or a < x0);then
            0 < x0 - a or 0 < a - x0 by XREAL_1:57;then
            a < a + (x0 -a) or 0 < a - x0 by XREAL_1:31;then
            a < x0 or x0 < x0 + (a - x0) by XREAL_1:31;
            hence contradiction by A136,A138;
          end;
A139:     now assume
A140:       not (x0 = b or x0 < b);then
            0 < x0 - b or 0 < b - x0 by XREAL_1:57;then
            b < b + (x0 -b) or 0 < b - x0 by XREAL_1:31;then
            b < x0 or x0 < x0 + (b - x0) by XREAL_1:31;
            hence contradiction by A136,A140;
          end;
          not (x0 in {q where q is Real: a<q & q<b}) by A135,RCOMP_1:def 2;
          hence contradiction by A135,A137,A139;
        end;
        diff(y1,x0) = diff(y2,x0)
        proof
          per cases by A134;
          suppose
A142:       x0 = a;
            x0 in {r where r is Real: a <= r & r <= b} by A1,A142;then
A143:       x0 in [.a,b.] by RCOMP_1:def 1;then
A144:       y1 is_differentiable_in x0 by A1,FDIFF_1:16;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:16;then
A146:       y2 is_right_differentiable_in x0 &
            diff(y2,x0) = Rdiff(y2,x0) by FDIFF_3:22;
A147:       y1 - y2 is_right_differentiable_in x0 by A145,A146,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 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 holds h.n > 0);
A150:           h is convergent & lim h = 0 by FDIFF_1:def 1;
A151:           0 < b - x0 by A6,A142,XREAL_1:52;
                consider n such that
A152:           for m st n<=m holds abs(h.m - 0) < (b - x0)/2
                by A150,A151,SEQ_2:def 7;
A153:           for p1 st 0 < p1 ex n1 st for m st n1 <= m
                holds
                abs((h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m-0)<p1
                proof
                  let p1 such that
A154:             0 < p1;
                  take n;
                  for m st n <= m holds
                  (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m = 0
                  proof
                    let m such that
A155:               n <= m;
A156:               abs(h.m - 0) < (b - x0)/2 by A152,A155;
A157:               0 < h.m by A149;then
A158:               h.m < (b - x0)/2 by A156,ABSVALUE:def 1;
A159:               a + 0 <= x0 + h.m by A142,A157,XREAL_1:9;
                    x0 + h.m <= x0 + (b - x0)/2 by A158,XREAL_1:9;then
A160:               x0 + h.m + 0 <= b - (b - x0)/2 + (b - x0)/2
                    by A151,XREAL_1:9;
A161:               [.a,b.] c= dom y1 /\ dom y2 by A1,XBOOLE_1:19;then
                    x0 in dom y1 /\ dom y2 by A143;then
A162:               x0 in dom(y1-y2) by VALUED_1:12;
A163:               [.a,b.] c= dom(y1-y2) by A161,VALUED_1:12;
                    x0 + h.m in {r where r is Real : a <= r & r <= b }
                    by A159,A160;then
A164:               x0 + h.m in [.a,b.] by RCOMP_1:def 1;
A165:               x0 in rng c1 by A149,TARSKI:def 1;
A166:               lim c1 = c1.m by SEQ_4:41;
A167:               (h+c1).m = h.m + c1.m by SEQ_1:11
                    .= h.m + x0 by A166,A165,SEQ_4:40;
A168:               rng c1 c= dom (y1-y2)
                    proof
                      for x be set st x in rng c1
                      holds
                      x in dom (y1-y2)
                      by A162,A149,TARSKI:def 1;
                      hence thesis by TARSKI:def 3;
                    end;
A169:               (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m
                    = (h").m*((y1-y2)/*(h+c1) - (y1-y2)/*c1).m
                    by SEQ_1:12
                    .= (h").m*(((y1-y2)/*(h+c1)).m - ((y1-y2)/*c1).m )
                    by RFUNCT_2:6
                    .= (h").m*((y1-y2).((h+c1).m) - ((y1-y2)/*c1).m )
                    by A149,FUNCT_2:185
                    .= (h").m*((y1-y2).((h+c1).m) - (y1-y2).(c1.m) )
                    by A168,FUNCT_2:185
                    .= (h").m*((y1-y2).(h.m+x0) - (y1-y2).x0 )
                    by A165,A166,SEQ_4:40,A167;
A170:               (y1-y2).(h.m+x0)
                    = y1.(h.m+x0) - y2.(h.m+x0) by A163,A164,VALUED_1:13
                    .= (y1 | [.a,b.]).(h.m+x0) - y2.(h.m+x0)
                    by A164,FUNCT_1:72
                    .= (y1 | [.a,b.]).(h.m+x0) - (y2 | [.a,b.]).(h.m+x0)
                    by A164,FUNCT_1:72
                    .= 0 by A1;
                    (y1-y2).x0 = y1.x0 - y2.x0 by A162,VALUED_1:13
                    .= (y1 | [.a,b.]).x0 - y2.x0 by A143,FUNCT_1:72
                    .= (y1 | [.a,b.]).x0 - (y2 | [.a,b.]).x0
                    by A143,FUNCT_1:72
                    .= 0 by A1;
                    hence thesis by A169,A170;
                  end;
                  hence thesis by A154,COMPLEX1:130;
                end;
                (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1))
                is convergent by A153,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
A171:       x0 in ].a,b.[;
A172:       ].a,b.[ is open by RCOMP_1:25;
A173:       ].a,b.[ c= [.a,b.]
            proof
              for x0 be set st x0 in ].a,b.[ holds x0 in [.a,b.]
              proof
                let x0 be set such that
A174:           x0 in ].a,b.[;
                x0 in {r where r is Real : a < r & r < b }
                by A174,RCOMP_1:def 2;then
A175:           ex r st r = x0 & a < r & r < b;then
                reconsider x0 as Real;
                x0 in {r where r is Real : a <= r & r <= b } by A175;
                hence thesis by RCOMP_1:def 1;
              end;
              hence thesis by TARSKI:def 3;
            end;then
A176:       y1 is_differentiable_on ].a,b.[
            by A1,A172,XBOOLE_1:1,FDIFF_1:34;
            then
A177:       y1| (].a,b.[) is_differentiable_on ].a,b.[ &
            (y1| (].a,b.[))`| (].a,b.[) = y1`| (].a,b.[)
            by A172,FDIFF_2:16;
A178:       (y1`| (].a,b.[)).x0 = diff(y1,x0) by A171,A176,FDIFF_1:def 8;
A179:       y2 is_differentiable_on ].a,b.[
            by A1,A172,A173,XBOOLE_1:1,FDIFF_1:34;
            then
A180:       y2| (].a,b.[) is_differentiable_on ].a,b.[ &
            (y2| (].a,b.[))`| (].a,b.[) = y2`| (].a,b.[)
            by A172,FDIFF_2:16;
A181:       (y2`| (].a,b.[)).x0 = diff(y2,x0) by A171,A179,FDIFF_1:def 8;
A182:       dom (y1| (].a,b.[) )
            = dom y1 /\ (].a,b.[) by RELAT_1:90
            .= ].a,b.[ by A1,A173,XBOOLE_1:1,XBOOLE_1:28
            .= dom y2 /\ (].a,b.[) by A1,A173,XBOOLE_1:1,XBOOLE_1:28
            .= dom (y2| (].a,b.[) ) by RELAT_1:90;
            for x0 be set st x0 in dom (y1| (].a,b.[) )
            holds
            (y1| (].a,b.[) ).x0 = (y2| (].a,b.[) ).x0
            proof
              let x0 be set such that
A183:         x0 in dom (y1| (].a,b.[) );
A184:         dom (y1| (].a,b.[) )
              = dom y1 /\ (].a,b.[) by RELAT_1:90
              .= ].a,b.[ by A1,A173,XBOOLE_1:1,XBOOLE_1:28;
              (y1| (].a,b.[) ).x0
              = y1.x0 by A183,A184,FUNCT_1:72
              .= (y1| ([.a,b.]) ).x0 by A173,A183,A184,FUNCT_1:72
              .= y2.x0 by A173,A183,A184,FUNCT_1:72,A1
              .= (y2| (].a,b.[) ).x0 by A183,A184,FUNCT_1:72;
              hence thesis;
            end;
            hence thesis by A177,A178,A180,A181,A182,FUNCT_1:9;
          end;
          suppose
A185:       x0 = b;
            x0 in {r where r is Real: a <= r & r <= b} by A1,A185;then
A186:       x0 in [.a,b.] by RCOMP_1:def 1;then
A187:       y1 is_differentiable_in x0 by A1,FDIFF_1:16;then
A188:       y1 is_left_differentiable_in x0 &
            diff(y1,x0) = Ldiff(y1,x0) by FDIFF_3:22;
            y2 is_differentiable_in x0 by A1,A186,FDIFF_1:16;then
A189:       y2 is_left_differentiable_in x0 &
            diff(y2,x0) = Ldiff(y2,x0) by FDIFF_3:22;
A190:       y1 - y2 is_left_differentiable_in x0 by A188,A189,FDIFF_3:11;
            Ldiff(y1,x0) = Ldiff(y2,x0)
            proof
A191:         Ldiff(y1,x0) - Ldiff(y2,x0) = Ldiff(y1-y2,x0)
              by A188,A189,FDIFF_3:11;
              for h,c1 st rng c1 = {x0} & rng (h+c1) c= dom (y1-y2) &
              (for n holds h.n < 0) holds
              lim (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)) = 0
              proof
                let h,c1 such that
A192:           rng c1 = {x0} & rng (h+c1) c= dom (y1-y2) &
                (for n holds h.n < 0);
A193:           h is convergent & lim h = 0 by FDIFF_1:def 1;
A194:           0 < b - a by A6,XREAL_1:52;
                consider n such that
A195:           for m st n<=m holds abs(h.m - 0) < (x0 - a)/2
                by A185,A193,A194,SEQ_2:def 7;
A196:           for p1 st 0 < p1 ex n1 st for m st n1 <= m holds
                abs((h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m-0) < p1
                proof
                  let p1 such that
A197:             0 < p1;
                  take n;
                  for m st n <= m holds
                  (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m = 0
                  proof
                    let m such that
A198:               n <= m;
A199:               abs(h.m - 0) < (x0 - a)/2 by A195,A198;
A200:               h.m < 0 by A192;then
A201:               -h.m < (x0 - a)/2 by A199,ABSVALUE:def 1;
A202:               x0 + h.m <= b + 0 by A185,A200,XREAL_1:9;
                    x0 - (x0 - a)/2 <= x0 - (-h.m) by A201,XREAL_1:15;
                    then
A203:               a + (x0 - a)/2 - (x0 - a)/2 <= x0 + h.m - 0
                    by A185,A194,XREAL_1:15;
A204:               [.a,b.] c= dom y1 /\ dom y2 by A1,XBOOLE_1:19;then
                    x0 in dom y1 /\ dom y2 by A186;then
A205:               x0 in dom(y1-y2) by VALUED_1:12;
A206:               [.a,b.] c= dom(y1-y2) by A204,VALUED_1:12;
                    x0 + h.m in {r where r is Real : a <= r & r <= b }
                    by A202,A203;then
A207:               x0 + h.m in [.a,b.] by RCOMP_1:def 1;
                    x0 in rng c1 by A192,TARSKI:def 1;then
A208:               lim c1 = x0 by SEQ_4:40;
A209:               (h+c1).m = h.m + c1.m by SEQ_1:11
                    .= h.m + x0 by A208,SEQ_4:41;
A210:               rng c1 c= dom (y1-y2)
                    proof
                      for x be set st x in rng c1 holds
                      x in dom (y1-y2) by A192,A205,TARSKI:def 1;
                      hence thesis by TARSKI:def 3;
                    end;
A211:               (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m
                    = (h").m*((y1-y2)/*(h+c1) - (y1-y2)/*c1).m
                    by SEQ_1:12
                    .= (h").m*(((y1-y2)/*(h+c1)).m - ((y1-y2)/*c1).m )
                    by RFUNCT_2:6
                    .= (h").m*((y1-y2).((h+c1).m) - ((y1-y2)/*c1).m )
                    by A192,FUNCT_2:185
                    .= (h").m*((y1-y2).((h+c1).m) - (y1-y2).(c1.m) )
                    by A210,FUNCT_2:185
                    .= (h").m*((y1-y2).(h.m+x0) - (y1-y2).x0 )
                    by A208,SEQ_4:41,A209;
A212:               (y1-y2).(h.m+x0)
                    = y1.(h.m+x0) - y2.(h.m+x0) by A206,A207,VALUED_1:13
                    .= (y1 | [.a,b.]).(h.m+x0) - y2.(h.m+x0)
                    by A207,FUNCT_1:72
                    .= (y1 | [.a,b.]).(h.m+x0) - (y2 | [.a,b.]).(h.m+x0)
                    by A207,FUNCT_1:72
                    .= 0 by A1;
                    (y1-y2).x0 = y1.x0 - y2.x0 by A205,VALUED_1:13
                    .= (y1 | [.a,b.]).x0 - y2.x0 by A186,FUNCT_1:72
                    .= (y1 | [.a,b.]).x0 - (y2 | [.a,b.]).x0
                    by A186,FUNCT_1:72
                    .= 0 by A1;
                    hence thesis by A211,A212;
                  end;
                  hence thesis by A197,COMPLEX1:130;
                end; then
                (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1))
                is convergent by SEQ_2:def 6;
                hence thesis by A196,SEQ_2:def 7;
              end;then
              Ldiff(y1-y2,x0) = 0 by A190,FDIFF_3:def 5;
              hence thesis by A191;
            end;
            hence thesis by A187,A189,FDIFF_3:22;
          end;
        end;
        hence thesis by A128,A130,A131,A132,A133,FUNCT_1:72;
      end;
      hence thesis by A128,A129,FUNCT_1:def 17;
    end;
A213: (u01(#)(x1`|Z) - v01(#)(y1`|Z)) | AB
    = (u02(#)(x2`|Z) - v02(#)(y2`|Z)) | AB
    proof
A214: x1`|Z is PartFunc of REAL,COMPLEX &
      y1`|Z is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17;
A215: u01 is PartFunc of REAL,COMPLEX &
      v01 is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17;
      u01(#)(x1`|Z) is PartFunc of REAL,COMPLEX &
      v01(#)(y1`|Z) is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17;then
A216: (u01(#)(x1`|Z) - v01(#)(y1`|Z)) | AB
      = (u01(#)(x1`|Z)) | AB - (v01(#)(y1`|Z)) | AB by CFUNCT_1:67
      .= (u01| AB)(#)((x1`|Z)| AB) - (v01(#)(y1`|Z)) | AB
      by A214,A215,CFUNCT_1:65
      .= (u01| AB)(#)((x1`|Z)| AB) - (v01| AB)(#)((y1`|Z)| AB)
      by A214,A215,CFUNCT_1:65;
A217: x2`|Z is PartFunc of REAL,COMPLEX &
      y2`|Z is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17;
A218: u02 is PartFunc of REAL,COMPLEX &
      v02 is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17;
      u02(#)(x2`|Z) is PartFunc of REAL,COMPLEX &
      v02(#)(y2`|Z) is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17;
      then
      (u02(#)(x2`|Z) - v02(#)(y2`|Z)) | AB
      = (u02(#)(x2`|Z)) | AB - (v02(#)(y2`|Z)) | AB by CFUNCT_1:67
      .= (u02| AB)(#)((x2`|Z)| AB) - (v02(#)(y2`|Z)) | AB
      by A217,A218,CFUNCT_1:65
      .= (u02| AB)(#)((x2`|Z)| AB) - (v02| AB)(#)((y2`|Z)| AB)
      by A217,A218,CFUNCT_1:65;
      hence thesis by A7,A24,A110,A127,A216;
    end;
A219: 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 A213
    .= integral( u02(#)(x2`|Z) - v02(#)(y2`|Z),a,b ) by INTEGRA5:19;
A220: (v01(#)(x1`|Z) + u01(#)(y1`|Z)) | AB
    = (v02(#)(x2`|Z) + u02(#)(y2`|Z)) | AB
    proof
A221: x1`|Z is PartFunc of REAL,COMPLEX &
      y1`|Z is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:17;
A222: v01 is PartFunc of REAL,COMPLEX &
      u01 is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:17;
      v01(#)(x1`|Z) is PartFunc of REAL,COMPLEX &
      u01(#)(y1`|Z) is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17;
      then
A223: (v01(#)(x1`|Z) + u01(#)(y1`|Z)) | AB
      = (v01(#)(x1`|Z)) | AB + (u01(#)(y1`|Z)) | AB by CFUNCT_1:64
      .= (v01| AB)(#)((x1`|Z)| AB) + (u01(#)(y1`|Z)) | AB
      by A221,A222,CFUNCT_1:65
      .= (v01| AB)(#)((x1`|Z)| AB) + (u01| AB)(#)((y1`|Z)| AB)
      by A221,A222,CFUNCT_1:65;
A224: x2`|Z is PartFunc of REAL,COMPLEX &
      y2`|Z is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:17;
A225: v02 is PartFunc of REAL,COMPLEX &
      u02 is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:17;
      v02(#)(x2`|Z) is PartFunc of REAL,COMPLEX &
      u02(#)(y2`|Z) is PartFunc of REAL,COMPLEX
      by NUMBERS:11,RELSET_1:17; then
      (v02(#)(x2`|Z) + u02(#)(y2`|Z)) | AB
      = (v02(#)(x2`|Z)) | AB + (u02(#)(y2`|Z)) | AB by CFUNCT_1:64
      .= (v02| AB)(#)((x2`|Z)| AB) + (u02(#)(y2`|Z)) | AB
      by A224,A225,CFUNCT_1:65
      .= (v02| AB)(#)((x2`|Z)| AB) + (u02| AB)(#)((y2`|Z)| AB)
      by A224,A225,CFUNCT_1:65;
      hence thesis by A7,A24,A110,A127,A223;
    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 A220
    .= integral( v02(#)(x2`|Z) + u02(#)(y2`|Z),a,b) by INTEGRA5:19;
    hence thesis by A2,A3,A219;
  end;
  suppose
A227: a=b; then
    reconsider BA=[.b,a.] as closed-interval Subset of REAL
    by INTEGRA1:def 1;
A228: integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,a,b )
     = integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,BA) by A227,INTEGRA5:19;
A229: -integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,BA)
    = integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,a,b ) by INTEGRA5:20;
A230:integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,a,b )
    = integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,BA) by A227,INTEGRA5:19;
A231: -integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,BA)
    = integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,a,b ) by INTEGRA5:20;
A232: integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,a,b )
    = integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,BA) by A227,INTEGRA5:19;
A233: integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,a,b )
    = -integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,a,b ) by A232,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 A227,INTEGRA5:20;
    hence thesis by A2,A3,A228,A229,A230,A231,A233;
  end;
end;

definition
  let f be PartFunc of COMPLEX,COMPLEX;
  let C be C1-curve;
  assume
A1: rng C c= dom f;
  func integral(f,C) -> Complex means :Def4:
  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+<i>(#)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+<i>(#)y) | [.a,b.]  by Def3;
    take IT = 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+<i>(#)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+<i>(#)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+<i>(#)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+<i>(#)y2) | [.a2,b2.] &
    s2 = integral(f,x2,y2,a2,b2,Z2) by A4;
    dom C is closed-interval Subset of REAL by A5,INTEGRA1:def 1;
    then
A8: a1 = a2 & b1 = b2 by A6,A5,INTEGRA1:6;
    reconsider Z3 = Z1 /\ Z2 as Subset of REAL;
    reconsider ZZ1=Z1, ZZ2= Z2, ZZ3= Z3 as Subset of R^1 by TOPMETR:24;
    ZZ1 is open & ZZ2 is open by A5,A6,BORSUK_5:62;then
    ZZ1 /\ ZZ2 is open by TOPS_1:38; then
A9: Z3 is open by BORSUK_5:62;
A11: 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
A12:    x0 in [.a1,b1.];
A13:    dom(<i>(#)y1) = dom y1 by VALUED_1:def 5;
        dom(x1+<i>(#)y1) = dom x1 /\ dom(<i>(#)y1)
        by VALUED_1:def 1;then
A14:    [.a1,b1.] c= dom(x1+<i>(#)y1) by A5,A13,XBOOLE_1:19;
A15:    ((x1+<i>(#)y1) | [.a1,b1.]).x0
        = (x1+<i>(#)y1).x0 by A12,FUNCT_1:72
        .= x1.x0 + (<i>(#)y1).x0 by A12,A14,VALUED_1:def 1
        .= x1.x0 + <i>*y1.x0 by VALUED_1:6;
A16:    dom(<i>(#)y2) = dom y2 by VALUED_1:def 5;
A17:    dom(x2+<i>(#)y2) = dom x2 /\ dom(<i>(#)y2)
        by VALUED_1:def 1;
A18:    [.a2,b2.] c= dom(x2+<i>(#)y2) by A6,A16,A17,XBOOLE_1:19;
        ((x2+<i>(#)y2) | [.a2,b2.]).x0
        = (x2+<i>(#)y2).x0 by A6,A5,A12,FUNCT_1:72
        .= x2.x0 + (<i>(#)y2).x0 by A6,A5,A12,A18,VALUED_1:def 1
        .= x2.x0 + <i>*y2.x0 by VALUED_1:6;
        hence thesis by A6,A5,A15,COMPLEX1:163;
      end;
      hence thesis by A5,A6,FUNCT_1:165;
    end;
A19: 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
A20:    x0 in [.a1,b1.];
A21:    dom(<i>(#)y1) = dom y1 by VALUED_1:def 5;
        dom(x1+<i>(#)y1) = dom x1 /\ dom(<i>(#)y1)
        by VALUED_1:def 1;then
A22:    [.a1,b1.] c= dom(x1+<i>(#)y1) by A5,A21,XBOOLE_1:19;
A23:    ((x1+<i>(#)y1) | [.a1,b1.]).x0
        = (x1+<i>(#)y1).x0 by A20,FUNCT_1:72
        .= x1.x0 + (<i>(#)y1).x0 by A20,A22,VALUED_1:def 1
        .= x1.x0 + <i>*y1.x0 by VALUED_1:6;
A24:    dom(<i>(#)y2) = dom y2 by VALUED_1:def 5;
A25:    dom(x2+<i>(#)y2) = dom x2 /\ dom(<i>(#)y2)
        by VALUED_1:def 1;
A26:    [.a2,b2.] c= dom(x2+<i>(#)y2) by A6,A24,A25,XBOOLE_1:19;
        ((x2+<i>(#)y2) | [.a2,b2.]).x0
        = (x2+<i>(#)y2).x0 by A5,A6,A20,FUNCT_1:72
        .= x2.x0 + (<i>(#)y2).x0 by A5,A6,A20,A26,VALUED_1:def 1
        .= x2.x0 + <i>*y2.x0 by VALUED_1:6;
        hence thesis by A6,A5,A23,COMPLEX1:163;
      end;
      hence thesis by A5,A6,FUNCT_1:165;
    end;
A27: [.a1,b1.] c= Z3 by A5,A6,XBOOLE_1:19;
A28: x1 is_differentiable_on Z3 &
    y1 is_differentiable_on Z3 by A5,A9,XBOOLE_1:17,FDIFF_1:34;
A29: x2 is_differentiable_on Z3 &
    y2 is_differentiable_on Z3 by A6,A9,XBOOLE_1:17,FDIFF_1:34;
    thus s1 = integral(f,x1,y1,a1,b1,Z3) by A1,A5,A9,A27,Lm1,XBOOLE_1:17
    .= integral(f,x2,y2,a2,b2,Z3)
    by A1,A5,A6,A8,A9,A11,A19,A28,A29,Lm2,XBOOLE_1:19
    .= s2 by A1,A6,A5,A9,A27,Lm1,XBOOLE_1:17;
  end;
end;

definition
  let f be PartFunc of COMPLEX,COMPLEX;
  let C be C1-curve;
  pred f is_integrable_on C means :Def5:
  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+<i>(#)y) | [.a,b.] ) holds
  (u0(#)(x`|Z) - v0(#)(y`|Z)) is_integrable_on [' a,b '] &
  (v0(#)(x`|Z) + u0(#)(y`|Z)) is_integrable_on [' a,b '];
end;

definition
  let f be PartFunc of COMPLEX, COMPLEX;
  let C be C1-curve;
  pred f is_bounded_on C means :Def6:
  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+<i>(#)y) | [.a,b.] ) holds
  (u0(#)(x`|Z) - v0(#)(y`|Z))|[' a,b '] is bounded &
  (v0(#)(x`|Z) + u0(#)(y`|Z))|[' a,b '] is bounded;
end;

begin :: Linearity of Complex Intergal

theorem
  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+<i>(#)y) | [.a,b.] by Def3;
  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 )*<i> 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 )*<i> by Def2;
A5: integral(f,C) = integral(f,x,y,a,b,Z) &
  integral(g,C) = integral(g,x,y,a,b,Z) by A1,A2,Def4;
A6: dom (f+g) = dom f /\ dom g by VALUED_1:def 1;
A7: rng C c= dom f /\ dom g by A1, XBOOLE_1:19;
  consider u0,v0 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 )*<i> by Def2;
A9: u0(#)(x`|Z)  = uf0(#)(x`|Z) + ug0(#)(x`|Z)
  proof
A10: dom (uf0(#)(x`|Z) + ug0(#)(x`|Z))
    = dom (uf0(#)(x`|Z)) /\ dom (ug0(#)(x`|Z)) by VALUED_1:def 1
    .= (dom uf0 /\ dom (x`|Z)) /\ dom (ug0(#)(x`|Z)) by VALUED_1:def 4
    .= (dom uf0 /\ dom (x`|Z)) /\ (dom ug0 /\ dom (x`|Z))
    by VALUED_1:def 4
    .= dom uf0 /\ (dom (x`|Z) /\ (dom ug0 /\ dom (x`|Z))) by XBOOLE_1:16
    .= dom uf0 /\ ((dom (x`|Z) /\ dom (x`|Z)) /\ dom ug0) by XBOOLE_1:16
    .= (dom uf0 /\ dom ug0) /\ dom (x`|Z) by XBOOLE_1:16;
A11: dom (u0(#)(x`|Z)) = dom u0 /\ dom (x`|Z) by VALUED_1:def 4;
A12: dom u0 = dom uf0 /\ dom ug0
    proof
A13:  for x0 be set st x0 in dom u0
      holds x0 in dom uf0 /\ dom ug0
      proof
        let x0 be set 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:21;
        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:21;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:21;then
        x0 in dom uf0 & x0 in dom ug0 by A3,A4,A15,FUNCT_1:21;
        hence thesis by XBOOLE_0:def 4;
      end;
      for x0 be set st x0 in dom uf0 /\ dom ug0
      holds x0 in dom u0
      proof
        let x0 be set such that
A17:    x0 in dom uf0 /\ dom ug0;
A18:    x0 in dom uf0 & x0 in dom ug0 by A17,XBOOLE_0:def 4;
A19:    x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Re f)*(R2-to-C)) by A3,A18,FUNCT_1:21;
A20:    x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Re g)*(R2-to-C)) by A18,A4,FUNCT_1:21;
        set R2 = <:x,y:>.x0;
A21:    R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Re f) by A19,FUNCT_1:21;
        R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Re g) by A20,FUNCT_1:21;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:21;
        hence thesis by A8,A19,FUNCT_1:21;
      end;
      hence thesis by A13, TARSKI:2;
    end;
    for x0 be set st x0 in dom (u0(#)(x`|Z))
    holds (u0(#)(x`|Z)).x0 = (uf0(#)(x`|Z) + ug0(#)(x`|Z)).x0
    proof
      let x0 be set 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;
A24:  x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (f+g))*(R2-to-C))
      by A8,A23,FUNCT_1:21;
      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:21;
      set c0 = (R2-to-C).R2;
A26:  u0.x0 = ((Re (f+g))*(R2-to-C)).R2 by A8,A23,FUNCT_1:22
      .= (Re (f+g)).c0 by A24,FUNCT_1:22
      .= (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;
A29:  x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C))
      by A3,A28,FUNCT_1:21;
A30:  uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A28,FUNCT_1:22
      .= (Re f).c0 by A29,FUNCT_1:22;
A31:  x0 in dom <:x,y:> & R2 in dom ((Re g)*(R2-to-C))
      by A4,A28,FUNCT_1:21;
A32:  ug0.x0 = ((Re g)*(R2-to-C)).R2 by A4,A28,FUNCT_1:22
      .= (Re g).c0 by A31,FUNCT_1:22;
      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:9;
  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 set st x0 in dom v0 holds x0 in dom vf0 /\ dom vg0
      proof
        let x0 be set 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:21;
        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:21;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:21;then
        x0 in dom vf0 & x0 in dom vg0 by A3,A4,A42,FUNCT_1:21;
        hence thesis by XBOOLE_0:def 4;
      end;
      for x0 be set st x0 in dom vf0 /\ dom vg0 holds x0 in dom v0
      proof
        let x0 be set such that
A44:    x0 in dom vf0 /\ dom vg0;
A45:    x0 in dom vf0 & x0 in dom vg0 by A44,XBOOLE_0:def 4;
A46:    x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Im f)*(R2-to-C)) by A45,A3,FUNCT_1:21;
A47:    x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Im g)*(R2-to-C)) by A45,A4,FUNCT_1:21;
        set R2 = <:x,y:>.x0;
A48:    R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Im f) by A46,FUNCT_1:21;
        R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Im g) by A47,FUNCT_1:21;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:21;
        hence thesis by A8,A46,FUNCT_1:21;
      end;
      hence thesis by A40,TARSKI:2;
    end;
    for x0 be set st x0 in dom (v0(#)(x`|Z))
    holds (v0(#)(x`|Z)).x0 = (vf0(#)(x`|Z) + vg0(#)(x`|Z)).x0
    proof
      let x0 be set 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;
A51:  x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (f+g))*(R2-to-C))
      by A8,A50,FUNCT_1:21;
      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:21;
      set c0 = (R2-to-C).R2;
A53:  v0.x0 = ((Im (f+g))*(R2-to-C)).R2 by A8,A50,FUNCT_1:22
      .= (Im (f+g)).c0 by A51,FUNCT_1:22
      .= (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;
A56:  x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C))
      by A3,A55,FUNCT_1:21;
A57:  vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A55,FUNCT_1:22
      .= (Im f).c0 by A56,FUNCT_1:22;
A58:  x0 in dom <:x,y:> & R2 in dom ((Im g)*(R2-to-C))
      by A4,A55,FUNCT_1:21;
A59:  vg0.x0 = ((Im g)*(R2-to-C)).R2 by A4,A55,FUNCT_1:22
      .= (Im g).c0 by A58,FUNCT_1:22;
      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:9;
  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 set st x0 in dom u0 holds x0 in dom uf0 /\ dom ug0
      proof
        let x0 be set 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:21;
        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:21;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:21;then
        x0 in dom uf0 & x0 in dom ug0 by A3,A4,A69,FUNCT_1:21;
        hence thesis by XBOOLE_0:def 4;
      end;
      for x0 be set st x0 in dom uf0 /\ dom ug0 holds x0 in dom u0
      proof
        let x0 be set such that
A71:    x0 in dom uf0 /\ dom ug0;
A72:    x0 in dom uf0 & x0 in dom ug0 by A71,XBOOLE_0:def 4;
A73:    x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Re f)*(R2-to-C)) by A72,A3,FUNCT_1:21;
A74:    x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Re g)*(R2-to-C)) by A72,A4,FUNCT_1:21;
        set R2 = <:x,y:>.x0;
A75:    R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Re f) by A73,FUNCT_1:21;
        R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Re g) by A74,FUNCT_1:21;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:21;
        hence thesis by A8,A73,FUNCT_1:21;
      end;
      hence thesis by A67,TARSKI:2;
    end;
    for x0 be set st x0 in dom (u0(#)(y`|Z))
    holds (u0(#)(y`|Z)).x0 = (uf0(#)(y`|Z) + ug0(#)(y`|Z)).x0
    proof
      let x0 be set 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;
A78:  x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (f+g))*(R2-to-C))
      by A8,A77,FUNCT_1:21;
      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:21;
      set c0 = (R2-to-C).R2;
A80:  u0.x0 = ((Re (f+g))*(R2-to-C)).R2 by A8,A77,FUNCT_1:22
      .= (Re (f+g)).c0 by A78,FUNCT_1:22
      .= (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;
A83:  x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C))
      by A3,A82,FUNCT_1:21;
A84:  uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A82,FUNCT_1:22
      .= (Re f).c0 by A83,FUNCT_1:22;
A85:  x0 in dom <:x,y:> & R2 in dom ((Re g)*(R2-to-C))
      by A4,A82,FUNCT_1:21;
A86:  ug0.x0 = ((Re g)*(R2-to-C)).R2 by A4,A82,FUNCT_1:22
      .= (Re g).c0 by A85,FUNCT_1:22;
      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:9;
  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 set st x0 in dom v0 holds x0 in dom vf0 /\ dom vg0
      proof
        let x0 be set 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:21;
        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:21;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:21;then
        x0 in dom vf0 & x0 in dom vg0 by A3,A4,A96,FUNCT_1:21;
        hence thesis by XBOOLE_0:def 4;
      end;
      for x0 be set st x0 in dom vf0 /\ dom vg0 holds x0 in dom v0
      proof
        let x0 be set such that
A98:    x0 in dom vf0 /\ dom vg0;
A99:    x0 in dom vf0 & x0 in dom vg0 by A98,XBOOLE_0:def 4;
A100:   x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Im f)*(R2-to-C)) by A99,A3,FUNCT_1:21;
A101:   x0 in dom <:x,y:> &
        <:x,y:>.x0 in dom ((Im g)*(R2-to-C)) by A99,A4,FUNCT_1:21;
        set R2 = <:x,y:>.x0;
A102:   R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Im f) by A100,FUNCT_1:21;
        R2 in dom (R2-to-C) &
        (R2-to-C).R2 in dom (Im g) by A101,FUNCT_1:21;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:21;
        hence thesis by A8,A100,FUNCT_1:21;
      end;
      hence thesis by A94,TARSKI:2;
    end;
    for x0 be set st x0 in dom (v0(#)(y`|Z))
    holds (v0(#)(y`|Z)).x0 = (vf0(#)(y`|Z) + vg0(#)(y`|Z)).x0
    proof
      let x0 be set 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;
A105: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (f+g))*(R2-to-C))
      by A8,A104,FUNCT_1:21;
      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:21;
      set c0 = (R2-to-C).R2;
A107: v0.x0 = ((Im (f+g))*(R2-to-C)).R2 by A8,A104,FUNCT_1:22
      .= (Im (f+g)).c0 by A105,FUNCT_1:22
      .= (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;
A110: x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C))
      by A3,A109,FUNCT_1:21;
A111: vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A109,FUNCT_1:22
      .= (Im f).c0 by A110,FUNCT_1:22;
A112: x0 in dom <:x,y:> & R2 in dom ((Im g)*(R2-to-C))
      by A4,A109,FUNCT_1:21;
A113: vg0.x0 = ((Im g)*(R2-to-C)).R2 by A4,A109,FUNCT_1:22
      .= (Im g).c0 by A112,FUNCT_1:22;
      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:9;
  end;
A117: [.a,b.] c= dom uf0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom uf0
    proof
      let x0 be set such that
A118: x0 in [.a,b.];
A119: C.x0 in rng C by A2,A118,FUNCT_1:12;
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 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A121,FUNCT_3:68;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 (<i>(#)y) by A120,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A2,A118,XBOOLE_0:def 4;
      then
A124: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A125: [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A126: x.x0 = [x.x0,y.x0]`1 &
      y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A118,FUNCT_1:72,A2
      .= x.x0+(<i>(#)y).x0 by A124,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A125,A126,Def1
      .= (R2-to-C).R2 by A121,FUNCT_3:68;then
      (R2-to-C).R2 in dom f by A1,A119;then
      (R2-to-C).R2 in dom (Re f) by MESFUN6C:def 1;then
      R2 in dom ((Re f)* (R2-to-C)) by A123,FUNCT_1:21;
      hence thesis by A3,A122,FUNCT_1:21;
    end;
    hence thesis by TARSKI:def 3;
  end;
A127: [.a,b.] c= dom vf0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom vf0
    proof
      let x0 be set such that
A128: x0 in [.a,b.];
A129: C.x0 in rng C by A2,A128,FUNCT_1:12;
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 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A131,FUNCT_3:68;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 (<i>(#)y) by A130,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A2,A128,XBOOLE_0:def 4;
      then
A134: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A135: [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A136: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A128,FUNCT_1:72,A2
      .= x.x0+(<i>(#)y).x0 by A134,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A135,A136,Def1
      .= (R2-to-C).R2 by A131,FUNCT_3:68;then
      (R2-to-C).R2 in dom f by A1,A129;then
      (R2-to-C).R2 in dom (Im f) by MESFUN6C:def 2;then
      R2 in dom ((Im f)* (R2-to-C)) by A133,FUNCT_1:21;
      hence thesis by A3,A132,FUNCT_1:21;
    end;
    hence thesis by TARSKI:def 3;
  end;
A137: [.a,b.] c= dom ug0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom ug0
    proof
      let x0 be set such that
A138: x0 in [.a,b.];
A139: C.x0 in rng C by A138,A2,FUNCT_1:12;
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 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A141,FUNCT_3:68;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 (<i>(#)y) by A140,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A2,A138,XBOOLE_0:def 4;
      then
A144: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A145: [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A146: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A138,FUNCT_1:72,A2
      .= x.x0+(<i>(#)y).x0 by A144,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A145,A146,Def1
      .= (R2-to-C).R2 by A141,FUNCT_3:68;then
      (R2-to-C).R2 in dom g by A1,A139;then
      (R2-to-C).R2 in dom (Re g) by MESFUN6C:def 1;then
      R2 in dom ((Re g)* (R2-to-C)) by A143,FUNCT_1:21;
      hence thesis by A4,A142,FUNCT_1:21;
    end;
    hence thesis by TARSKI:def 3;
  end;
A147: [.a,b.] c= dom vg0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom vg0
    proof
      let x0 be set such that
A148: x0 in [.a,b.];
A149: C.x0 in rng C by A2,A148,FUNCT_1:12;
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 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A151,FUNCT_3:68;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 (<i>(#)y) by A150,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A2,A148,XBOOLE_0:def 4;
      then
A154: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A155: [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A156: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A148,FUNCT_1:72,A2
      .= x.x0+(<i>(#)y).x0 by A154,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A155,A156,Def1
      .= (R2-to-C).R2 by A151,FUNCT_3:68;then
      (R2-to-C).R2 in dom g by A1,A149;then
      (R2-to-C).R2 in dom (Im g) by MESFUN6C:def 2;then
      R2 in dom ((Im g)* (R2-to-C)) by A153,FUNCT_1:21;
      hence thesis by A4,A152,FUNCT_1:21;
    end;
    hence thesis by TARSKI:def 3;
  end;
A157: [' a,b '] c= dom (uf0(#)(x`|Z) - vf0(#)(y`|Z))
  proof
A158: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 4;
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 8
    .= dom uf0 /\ (Z /\ (Z /\ dom vf0)) by A2,FDIFF_1:def 8
    .= 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 4;
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 8
    .= dom ug0 /\ (Z /\ (Z /\ dom vg0)) by A2,FDIFF_1:def 8
    .= 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 4;
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 8
    .= dom vf0 /\ (Z /\ (Z /\ dom uf0)) by A2,FDIFF_1:def 8
    .= 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 4;
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 8
    .= dom vg0 /\ (Z /\ (Z /\ dom ug0)) by A2,FDIFF_1:def 8
    .= 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;
A169: (uf0(#)(x`|Z) - vf0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2,Def5;
A170: (ug0(#)(x`|Z) - vg0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2,Def5;
A171: (vf0(#)(x`|Z) + uf0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2,Def5;
A172: (vg0(#)(x`|Z) + ug0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2,Def5;
A173: (uf0(#)(x`|Z) - vf0(#)(y`|Z))|[' a,b '] is bounded by A1,A2,Def6;
A174: (ug0(#)(x`|Z) - vg0(#)(y`|Z))|[' a,b '] is bounded by A1,A2,Def6;
A175: (vf0(#)(x`|Z) + uf0(#)(y`|Z))|[' a,b '] is bounded by A1,A2,Def6;
A176: (vg0(#)(x`|Z) + ug0(#)(y`|Z))|[' a,b '] is bounded by A1,A2,Def6;
  integral(f+g,C)
  = integral(uf0(#)(x`|Z)+ug0(#)(x`|Z)-(vf0(#)(y`|Z)+vg0(#)(y`|Z)),a,b )
  + integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+(uf0(#)(y`|Z)+ug0(#)(y`|Z)),a,b )*<i>
  by A36,A63,A9,A90,A8,A2,A6,A7,Def4
  .= integral(uf0(#)(x`|Z)+ug0(#)(x`|Z)-vf0(#)(y`|Z)-vg0(#)(y`|Z),a,b )
  + integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+(uf0(#)(y`|Z)+ug0(#)(y`|Z)),a,b )*<i>
  by RFUNCT_1:32
  .= integral(uf0(#)(x`|Z)+ug0(#)(x`|Z)-vf0(#)(y`|Z)-vg0(#)(y`|Z),a,b )
  + integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+uf0(#)(y`|Z)+ug0(#)(y`|Z),a,b )*<i>
  by RFUNCT_1:19
  .= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z)+ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
  + integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+uf0(#)(y`|Z)+ug0(#)(y`|Z),a,b )*<i>
  by RFUNCT_1:19
  .= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z) + ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
  + integral(vf0(#)(x`|Z)+uf0(#)(y`|Z) + vg0(#)(x`|Z)+ug0(#)(y`|Z),a,b )*<i>
  by RFUNCT_1:19
  .= integral((uf0(#)(x`|Z)-vf0(#)(y`|Z)) + (ug0(#)(x`|Z)-vg0(#)(y`|Z)),a,b )
  + integral(vf0(#)(x`|Z)+uf0(#)(y`|Z) + vg0(#)(x`|Z)+ug0(#)(y`|Z),a,b )*<i>
  by RFUNCT_1:19
  .= integral((uf0(#)(x`|Z)-vf0(#)(y`|Z))
  + (ug0(#)(x`|Z)-vg0(#)(y`|Z)),a,b )
  + integral((vf0(#)(x`|Z)+uf0(#)(y`|Z))
  + (vg0(#)(x`|Z)+ug0(#)(y`|Z)),a,b )*<i> by RFUNCT_1:19
  .= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z),a,b )
  + integral(ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
  + integral((vf0(#)(x`|Z)+uf0(#)(y`|Z))
  + (vg0(#)(x`|Z)+ug0(#)(y`|Z)),a,b )*<i>
  by A2,A157,A160,A169,A170,A173,A174,INTEGRA6:12
  .= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z),a,b )
  + integral(ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
  + (integral(vf0(#)(x`|Z)+uf0(#)(y`|Z),a,b )
  + integral(vg0(#)(x`|Z)+ug0(#)(y`|Z),a,b ))*<i>
  by A2,A163,A166,A171,A172,A175,A176,INTEGRA6:12
  .= integral(f,C) + integral(g,C) by A4,A5,A3;
  hence thesis;
end;

theorem
  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+<i>(#)y) | [.a,b.] by Def3;
  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 )*<i> 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 )*<i> by Def2;
A6: dom u0 = dom uf0
  proof
A7: for x0 be set st x0 in dom u0 holds x0 in dom uf0
    proof
      let x0 be set 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:21;
      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:21;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:21;
      hence thesis by A3,A9,FUNCT_1:21;
    end;
    for x0 be set st x0 in dom uf0 holds x0 in dom u0
    proof
      let x0 be set 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:21;
      set R2 = <:x,y:>.x0;
A13:  R2 in dom (R2-to-C) &
      (R2-to-C).R2 in dom (Re f) by A12,FUNCT_1:21;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:21;
      hence thesis by A5,A12,FUNCT_1:21;
    end;
    hence thesis by A7,TARSKI:2;
  end;
A14: dom v0 = dom vf0
  proof
A15: for x0 be set st x0 in dom v0 holds x0 in dom vf0
    proof
      let x0 be set 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:21;
      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:21;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:21;
      hence thesis by A3,A17,FUNCT_1:21;
    end;
    for x0 be set st x0 in dom vf0 holds x0 in dom v0
    proof
      let x0 be set 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:21;
      set R2 = <:x,y:>.x0;
A21:  R2 in dom (R2-to-C) &
      (R2-to-C).R2 in dom (Im f) by A20,FUNCT_1:21;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:21;
      hence thesis by A5,A20,FUNCT_1:21;
    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:25
    .= 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 set st x0 in dom (u0(#)(x`|Z))
    holds (u0(#)(x`|Z)).x0 = (r(#)(uf0(#)(x`|Z))).x0
    proof
      let x0 be set 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;
A29:  x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (r(#)f))*(R2-to-C))
      by A5,A28,FUNCT_1:21;
      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:22
      .= (Re (r(#)f)).c0 by A29,FUNCT_1:22
      .= (r(#)Re f).c0 by MESFUN6C:2;
A31:  x0 in dom uf0 by A6,A27,XBOOLE_0:def 4;
A32:  x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C)) by A3,A31,FUNCT_1:21;
A33:  uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A6,A28,FUNCT_1:22
      .= (Re f).c0 by A32,FUNCT_1:22;
A34:  x0 in dom (uf0(#)(r(#)(x`|Z))) by A26,A25,RFUNCT_1:25;then
      x0 in dom (uf0) /\ dom (r(#)(x`|Z)) by VALUED_1:def 4;
      then
A35:  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 A33
      .= uf0.x0*(r(#)(x`|Z)).x0 by A35,VALUED_1:def 5
      .= (uf0(#)(r(#)(x`|Z))).x0 by A34,VALUED_1:def 4
      .= (r(#)(uf0(#)(x`|Z))).x0 by RFUNCT_1:25;
      hence thesis;
    end;
    hence thesis by A6,A23,A24,FUNCT_1:9;
  end;
A36: v0(#)(x`|Z)  = r(#)(vf0(#)(x`|Z))
  proof
A37: dom (r(#)(vf0(#)(x`|Z)))
    = dom (vf0(#)(r(#)(x`|Z))) by RFUNCT_1:25
    .= dom(vf0) /\ dom (r(#)(x`|Z)) by VALUED_1:def 4
    .= dom vf0 /\ dom (x`|Z) by VALUED_1:def 5;
A38: dom (v0(#)(x`|Z)) = dom v0 /\ dom (x`|Z) by VALUED_1:def 4;
A39: dom (v0(#)(x`|Z)) = dom (r(#)(vf0(#)(x`|Z))) by A14,A37,VALUED_1:def 4;
    for x0 be set st x0 in dom (v0(#)(x`|Z))
    holds (v0(#)(x`|Z)).x0 = (r(#)(vf0(#)(x`|Z))).x0
    proof
      let x0 be set such that
A40:  x0 in dom (v0(#)(x`|Z));
A41:  x0 in dom v0 /\ dom (x`|Z) by A40,VALUED_1:def 4;then
A42:  x0 in dom v0 & x0 in dom (x`|Z) by XBOOLE_0:def 4;
A43:  x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (r(#)f))*(R2-to-C))
      by A5,A42,FUNCT_1:21;
      set R2 = <:x,y:>.x0;
      set c0 = (R2-to-C).R2;
A44:  v0.x0 = ((Im (r(#)f))*(R2-to-C)).R2 by A5,A42,FUNCT_1:22
      .= (Im (r(#)f)).c0 by A43,FUNCT_1:22
      .= (r(#)Im f).c0 by MESFUN6C:2;
A45:  x0 in dom vf0 by A14,A41,XBOOLE_0:def 4;
A46:  x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C)) by A3,A45,FUNCT_1:21;
A47:  vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A14,A42,FUNCT_1:22
      .= (Im f).c0 by A46,FUNCT_1:22;
A48:  x0 in dom (vf0(#)(r(#)(x`|Z))) by A39,A40,RFUNCT_1:25;then
      x0 in dom (vf0) /\ dom (r(#)(x`|Z)) by VALUED_1:def 4; then
A49:  x0 in dom (r(#)(x`|Z)) by XBOOLE_0:def 4;
      (v0(#)(x`|Z)).x0 = (v0.x0)*((x`|Z).x0) by A40,VALUED_1:def 4
      .= (r*(Im f).c0)*((x`|Z).x0) by A44,VALUED_1:6
      .= vf0.x0*(r*((x`|Z).x0)) by A47
      .= vf0.x0*(r(#)(x`|Z)).x0 by A49,VALUED_1:def 5
      .= (vf0(#)(r(#)(x`|Z))).x0 by A48,VALUED_1:def 4
      .= (r(#)(vf0(#)(x`|Z))).x0 by RFUNCT_1:25;
      hence thesis;
    end;
    hence thesis by A14,A37,A38,FUNCT_1:9;
  end;
A50: u0(#)(y`|Z) = r(#)(uf0(#)(y`|Z))
  proof
A51: dom (r(#)(uf0(#)(y`|Z)))
    = dom (uf0(#)(r(#)(y`|Z))) by RFUNCT_1:25
    .= dom(uf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4
    .= dom uf0 /\ dom (y`|Z) by VALUED_1:def 5;
A52: dom (u0(#)(y`|Z)) = dom u0 /\ dom (y`|Z) by VALUED_1:def 4;
A53: dom (u0(#)(y`|Z)) = dom (r(#)(uf0(#)(y`|Z))) by A6,A51,VALUED_1:def 4;
    for x0 be set st x0 in dom (u0(#)(y`|Z))
    holds (u0(#)(y`|Z)).x0 = (r(#)(uf0(#)(y`|Z))).x0
    proof
      let x0 be set such that
A54:  x0 in dom (u0(#)(y`|Z));
A55:  x0 in dom u0 /\ dom (y`|Z) by A54,VALUED_1:def 4;then
A56:  x0 in dom u0 & x0 in dom (y`|Z) by XBOOLE_0:def 4;
A57:  x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (r(#)f))*(R2-to-C))
      by A5,A56,FUNCT_1:21;
      set R2 = <:x,y:>.x0;
      set c0 = (R2-to-C).R2;
A58:  u0.x0 = ((Re (r(#)f))*(R2-to-C)).R2 by A5,A56,FUNCT_1:22
      .= (Re (r(#)f)).c0 by A57,FUNCT_1:22
      .= (r(#)Re f).c0 by MESFUN6C:2;
A59:  x0 in dom uf0 by A6,A55,XBOOLE_0:def 4;
A60:  x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C)) by A3,A59,FUNCT_1:21;
A61:  uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A6,A56,FUNCT_1:22
      .= (Re f).c0 by A60,FUNCT_1:22;
A62:  x0 in dom (uf0(#)(r(#)(y`|Z))) by A53,A54,RFUNCT_1:25;then
      x0 in dom (uf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4;
      then
A63:  x0 in dom (r(#)(y`|Z)) by XBOOLE_0:def 4;
      (u0(#)(y`|Z)).x0 = (u0.x0)*((y`|Z).x0) by A54,VALUED_1:def 4
      .= (r*(Re f).c0)*((y`|Z).x0) by A58,VALUED_1:6
      .= uf0.x0*(r*((y`|Z).x0)) by A61
      .= uf0.x0*(r(#)(y`|Z)).x0 by A63,VALUED_1:def 5
      .= (uf0(#)(r(#)(y`|Z))).x0 by A62,VALUED_1:def 4
      .= (r(#)(uf0(#)(y`|Z))).x0 by RFUNCT_1:25;
      hence thesis;
    end;
    hence thesis by A6,A51,A52,FUNCT_1:9;
  end;
A64: v0(#)(y`|Z)  = r(#)(vf0(#)(y`|Z))
  proof
A65: dom (r(#)(vf0(#)(y`|Z)))
    = dom (vf0(#)(r(#)(y`|Z))) by RFUNCT_1:25
    .= dom(vf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4
    .= dom vf0 /\ dom (y`|Z) by VALUED_1:def 5;
A66: dom (v0(#)(y`|Z)) = dom v0 /\ dom (y`|Z) by VALUED_1:def 4;
A67: dom (v0(#)(y`|Z)) = dom (r(#)(vf0(#)(y`|Z))) by A14,A65,VALUED_1:def 4;
    for x0 be set st x0 in dom (v0(#)(y`|Z))
    holds (v0(#)(y`|Z)).x0 = (r(#)(vf0(#)(y`|Z))).x0
    proof
      let x0 be set such that
A68:  x0 in dom (v0(#)(y`|Z));
A69:  x0 in dom v0 /\ dom (y`|Z) by A68,VALUED_1:def 4;then
A70:  x0 in dom v0 & x0 in dom (y`|Z) by XBOOLE_0:def 4;
A71:  x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (r(#)f))*(R2-to-C))
      by A5,A70,FUNCT_1:21;
      set R2 = <:x,y:>.x0;
      set c0 = (R2-to-C).R2;
A72:  v0.x0 = ((Im (r(#)f))*(R2-to-C)).R2 by A5,A70,FUNCT_1:22
      .= (Im (r(#)f)).c0 by A71,FUNCT_1:22
      .= (r(#)Im f).c0 by MESFUN6C:2;
A73:  x0 in dom vf0 by A14,A69,XBOOLE_0:def 4;
A74:  x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C)) by A3,A73,FUNCT_1:21;
A75:  vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A14,A70,FUNCT_1:22
      .= (Im f).c0 by A74,FUNCT_1:22;
A76:  x0 in dom (vf0(#)(r(#)(y`|Z))) by A67,A68,RFUNCT_1:25;then
      x0 in dom (vf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4;
      then
A77:  x0 in dom (r(#)(y`|Z)) by XBOOLE_0:def 4;
      (v0(#)(y`|Z)).x0 = (v0.x0)*((y`|Z).x0) by A68,VALUED_1:def 4
      .= (r*(Im f).c0)*((y`|Z).x0) by A72,VALUED_1:6
      .= vf0.x0*(r*((y`|Z).x0)) by A75
      .= vf0.x0*(r(#)(y`|Z)).x0 by A77,VALUED_1:def 5
      .= (vf0(#)(r(#)(y`|Z))).x0 by A76,VALUED_1:def 4
      .= (r(#)(vf0(#)(y`|Z))).x0 by RFUNCT_1:25;
      hence thesis;
    end;
    hence thesis by A14,A65,A66,FUNCT_1:9;
  end;
A78: [.a,b.] c= dom uf0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom uf0
    proof
      let x0 be set such that
A79:  x0 in [.a,b.];
A80:  C.x0 in rng C by A2,A79,FUNCT_1:12;
A81:  x0 in dom x & x0 in dom y by A2,A79;
A82:  x0 in dom x /\ dom y by A2,A79,XBOOLE_0:def 4;then
A83:  x0 in dom <:x,y:> by FUNCT_3:def 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A82,FUNCT_3:68;then
      R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A84:  R2 in dom (R2-to-C) by FUNCT_2:def 1;
      x0 in dom (<i>(#)y) by A81,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A2,A79,XBOOLE_0:def 4;
      then
A85:  x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A86:  [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A87:  x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A79,FUNCT_1:72,A2
      .= x.x0+(<i>(#)y).x0 by A85,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A86,A87,Def1
      .= (R2-to-C).R2 by A82,FUNCT_3:68;then
      (R2-to-C).R2 in dom f by A1,A80;then
      (R2-to-C).R2 in dom (Re f) by MESFUN6C:def 1;then
      R2 in dom ((Re f)* (R2-to-C)) by A84,FUNCT_1:21;
      hence thesis by A3,A83,FUNCT_1:21;
    end;
    hence thesis by TARSKI:def 3;
  end;
A88: [.a,b.] c= dom vf0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom vf0
    proof
      let x0 be set such that
A89:  x0 in [.a,b.];
A90:  C.x0 in rng C by A2,A89,FUNCT_1:12;
A91:  x0 in dom x & x0 in dom y by A2,A89;
A92:  x0 in dom x /\ dom y by A2,A89,XBOOLE_0:def 4;then
A93:  x0 in dom <:x,y:> by FUNCT_3:def 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A92,FUNCT_3:68;then
      R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A94:  R2 in dom (R2-to-C) by FUNCT_2:def 1;
      x0 in dom (<i>(#)y) by A91,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A2,A89,XBOOLE_0:def 4; then
A95:  x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A96:  [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A97:  x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A89,FUNCT_1:72,A2
      .= x.x0+(<i>(#)y).x0 by A95,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A96,A97,Def1
      .= (R2-to-C).R2 by A92,FUNCT_3:68; then
      (R2-to-C).R2 in dom f by A1,A90;then
      (R2-to-C).R2 in dom (Im f) by MESFUN6C:def 2;then
      R2 in dom ((Im f)* (R2-to-C)) by A94,FUNCT_1:21;
      hence thesis by A3,A93,FUNCT_1:21;
    end;
    hence thesis by TARSKI:def 3;
  end;
A98: [' a,b '] c= dom (uf0(#)(x`|Z) - vf0(#)(y`|Z))
  proof
A99: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 4;
A100: 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 8
    .= dom uf0 /\ (Z /\ (Z /\ dom vf0)) by A2,FDIFF_1:def 8
    .= 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 A78,A88,XBOOLE_1:19;
    hence thesis by A2,A99,A100,XBOOLE_1:19;
  end;
A101: [' a,b '] c= dom (vf0(#)(x`|Z) + uf0(#)(y`|Z))
  proof
A102: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 4;
A103: 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 8
    .= dom vf0 /\ (Z /\ (Z /\ dom uf0)) by A2,FDIFF_1:def 8
    .= 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 A78,A88,XBOOLE_1:19;
    hence thesis by A2,A102,A103,XBOOLE_1:19;
  end;
A104: (uf0(#)(x`|Z) - vf0(#)(y`|Z)) is_integrable_on [' a,b ']
  by A1,A2,Def5;
A105: (vf0(#)(x`|Z) + uf0(#)(y`|Z)) is_integrable_on [' a,b ']
  by A1,A2,Def5;
A106: (uf0(#)(x`|Z) - vf0(#)(y`|Z))|[' a,b '] is bounded
  by A1,A2,Def6;
A107: (vf0(#)(x`|Z) + uf0(#)(y`|Z))|[' a,b '] is bounded
  by A1,A2,Def6;
  integral(r(#)f,C) = integral( r(#)(uf0(#)(x`|Z)) - r(#)(vf0(#)(y`|Z)),a,b )
  + integral( r(#)(vf0(#)(x`|Z)) + r(#)(uf0(#)(y`|Z)),a,b )*<i>
    by A36,A64,A50,A22,A5,A1,A2,A4,Def4
  .= integral(r(#)(uf0(#)(x`|Z) - vf0(#)(y`|Z)),a,b )
  + integral(r(#)(vf0(#)(x`|Z)) + r(#)(uf0(#)(y`|Z)),a,b )*<i> by RFUNCT_1:30
  .= integral(r(#)(uf0(#)(x`|Z) - vf0(#)(y`|Z)),a,b )
  + integral(r(#)(vf0(#)(x`|Z) + uf0(#)(y`|Z)),a,b )*<i> by RFUNCT_1:28
  .= r*integral(uf0(#)(x`|Z) - vf0(#)(y`|Z),a,b )
  + integral(r(#)(vf0(#)(x`|Z) + uf0(#)(y`|Z)),a,b )*<i>
  by A2,A98,A104,A106,INTEGRA6:10
  .= r*integral(uf0(#)(x`|Z) - vf0(#)(y`|Z),a,b )
  + r*integral(vf0(#)(x`|Z) + uf0(#)(y`|Z),a,b )*<i>
  by A2,A101,A105,A107,INTEGRA6:10
  .= r*(integral(uf0(#)(x`|Z) - vf0(#)(y`|Z),a,b )
  + integral(vf0(#)(x`|Z) + uf0(#)(y`|Z),a,b )*<i>)
  .= r*integral(f,C) by A1,A2,A3,Def4;
  hence thesis;
end;

begin :: Complex Integral of Complex Curve's Connection

theorem
  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+<i>(#)y) | [.a0,b0.] by Def3;
A4: a0 = a & b0 = b
  proof
    thus a0 = inf [.a0,b0.] by A3,XXREAL_2:25
    .= a by A1,XXREAL_2:25,A3;
    thus b0 = sup [.a0,b0.] by A3,XXREAL_2:29
    .= b by A1,XXREAL_2:29,A3;
  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 )*<i> 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+<i>(#)y1) | [.a1,b1.] by Def3;
A7: a1 = a & b1 = d
  proof
    thus a1 = inf [.a1,b1.] by A6,XXREAL_2:25
    .= a by A2,XXREAL_2:25,A1,A6;
    thus b1 = sup [.a1,b1.] by A6,XXREAL_2:29
    .= d by A2,XXREAL_2:29,A1,A6;
  end;
A8: rng C1 c= dom f
  proof
A9: [.a,d.] c= [.a,b.] by A2,XXREAL_1:34;
    for y0 be set st y0 in rng C1 holds y0 in rng C
    proof
      let y0 be set such that
A10:  y0 in rng C1;
      consider x0 be set such that
A11:  x0 in dom C1 & y0 = C1.x0 by A10,FUNCT_1:def 5;
      C1.x0 = C.x0 by A1,A11;
      hence thesis by A1,A9,A11,FUNCT_1:12;
    end;then
    rng C1 c= rng C by TARSKI:def 3;
    hence thesis by A1,XBOOLE_1:1;
  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+<i>(#)y2) | [.a2,b2.] by Def3;
A13: a2 = d & b2 = b
  proof
    thus a2 = inf [.a2,b2.] by A12,XXREAL_2:25
    .= d by A2,XXREAL_2:25,A1,A12;
    thus b2 = sup [.a2,b2.] by A12,XXREAL_2:29
    .= b by A2,XXREAL_2:29,A1,A12;
  end;
  rng C2 c= dom f
  proof
A14: [.d,b.] c= [.a,b.] by A2,XXREAL_1:34;
    for y0 be set st y0 in rng C2 holds y0 in rng C
    proof
      let y0 be set such that
A15:  y0 in rng C2;
      consider x0 be set such that
A16:  x0 in dom C2 & y0 = C2.x0 by A15,FUNCT_1:def 5;
      C2.x0 = C.x0 by A1,A16;
      hence thesis by A1,A14,A16,FUNCT_1:12;
    end;then
    rng C2 c= rng C by TARSKI:def 3;
    hence thesis by A1,XBOOLE_1:1;
  end;then
A17: integral(f,C2) = integral(f,x2,y2,d,b,Z2) by A12,A13,Def4;
A18: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 4;
A19: [' a,b '] c= dom u0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom u0
    proof
      let x0 be set such that
A20:  x0 in [.a,b.];
A21:  C.x0 in rng C by A3,A4,A20,FUNCT_1:12;
A22:  x0 in dom x & x0 in dom y by A3,A4,A20;
A23:  x0 in dom x /\ dom y by A3,A4,A20,XBOOLE_0:def 4;then
A24:  x0 in dom <:x,y:> by FUNCT_3:def 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A23,FUNCT_3:68;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 (<i>(#)y) by A22,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A3,A4,A20,XBOOLE_0:def 4;
      then
A26:  x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A27:  [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A28:  x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A20,FUNCT_1:72,A3,A4
      .= x.x0+(<i>(#)y).x0 by A26,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A27,A28,Def1
      .= (R2-to-C).R2 by A23,FUNCT_3:68; then
      (R2-to-C).R2 in dom f by A1,A21;then
      (R2-to-C).R2 in dom (Re f) by MESFUN6C:def 1;then
      R2 in dom ((Re f)* (R2-to-C)) by A25,FUNCT_1:21;
      hence thesis by A5,A24,FUNCT_1:21;
    end;
    hence thesis by A18,TARSKI:def 3;
  end;
A29: [' a,b '] c= dom v0
  proof
    for x0 be set st x0 in [.a,b.] holds x0 in dom v0
    proof
      let x0 be set such that
A30:  x0 in [.a,b.];
A31:  C.x0 in rng C by A3,A4,A30,FUNCT_1:12;
A32:  x0 in dom x & x0 in dom y by A3,A4,A30;
A33:  x0 in dom x /\ dom y by A3,A4,A30,XBOOLE_0:def 4;then
A34:  x0 in dom <:x,y:> by FUNCT_3:def 8;
      set R2 = <:x,y:>.x0;
      R2 = [x.x0,y.x0] by A33,FUNCT_3:68;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 (<i>(#)y) by A32,VALUED_1:def 5;then
      x0 in dom x /\ dom (<i>(#)y) by A3,A4,A30,XBOOLE_0:def 4; then
A36:  x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A37:  [x.x0,y.x0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A38:  x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2 by MCART_1:7;
      C.x0 = (x+<i>(#)y).x0 by A30,FUNCT_1:72,A3,A4
      .= x.x0+(<i>(#)y).x0 by A36,VALUED_1:def 1
      .= x.x0+<i>*y.x0 by VALUED_1:6
      .= (R2-to-C).([x.x0,y.x0]) by A37,A38,Def1
      .= (R2-to-C).R2 by A33,FUNCT_3:68; then
      (R2-to-C).R2 in dom f by A1,A31;then
      (R2-to-C).R2 in dom (Im f) by MESFUN6C:def 2;then
      R2 in dom ((Im f)* (R2-to-C)) by A35,FUNCT_1:21;
      hence thesis by A5,A34,FUNCT_1:21;
    end;
    hence thesis by A18,TARSKI:def 3;
  end;
A39: (u0(#)(x`|Z) - v0(#)(y`|Z)) is_integrable_on [' a,b '] &
  (v0(#)(x`|Z) + u0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A3,Def5;
A40: (u0(#)(x`|Z) - v0(#)(y`|Z))|[' a,b '] is bounded &
  (v0(#)(x`|Z) + u0(#)(y`|Z))|[' a,b '] is bounded by A1,A3,Def6;
A41: [' a,b '] c= dom (u0(#)(x`|Z) - v0(#)(y`|Z))
  proof
A42: dom (u0(#)(x`|Z) - v0(#)(y`|Z))
    = dom (u0(#)(x`|Z)) /\ dom (v0(#)(y`|Z)) by VALUED_1:12
    .= (dom u0 /\ dom(x`|Z)) /\ dom (v0(#)(y`|Z)) by VALUED_1:def 4
    .= (dom u0 /\ dom(x`|Z)) /\ (dom v0 /\ dom(y`|Z)) by VALUED_1:def 4
    .= (dom u0 /\ Z) /\ (dom v0 /\ dom(y`|Z)) by A3,FDIFF_1:def 8
    .= (dom u0 /\ Z) /\ (dom v0 /\ Z) by A3,FDIFF_1:def 8
    .= dom u0 /\ (Z /\ (dom v0 /\ Z)) by XBOOLE_1:16
    .= dom u0 /\ ((Z /\ Z) /\ dom v0) by XBOOLE_1:16
    .= (dom u0 /\ dom v0) /\ Z by XBOOLE_1:16;
A43: [' a,b '] c= dom u0 /\ dom v0 by A19,A29,XBOOLE_1:19;
    [' a,b '] c= Z by A1,A3,INTEGRA5:def 4;
    hence 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 8
    .= (dom v0 /\ Z) /\ (dom u0 /\ Z) by A3,FDIFF_1:def 8
    .= dom v0 /\ (Z /\ (dom u0 /\ Z)) by XBOOLE_1:16
    .= dom v0 /\ ((Z /\ Z) /\ dom u0) by XBOOLE_1:16
    .= (dom v0 /\ dom u0) /\ Z by XBOOLE_1:16;
A46: [' a,b '] c= dom v0 /\ dom u0 by A19,A29,XBOOLE_1:19;
    [' a,b '] c= Z by A1,A3,INTEGRA5:def 4;
    hence thesis by A45,A46,XBOOLE_1:19;
  end;
  reconsider AD=[.a,d.] as closed-interval Subset of REAL
  by A6,A7,INTEGRA1:def 1;
  reconsider DB=[.d,b.] as closed-interval Subset of REAL
  by A12,A13,INTEGRA1:def 1;
A47: integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,d )
  + integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,d )*<i>
  = integral( f,x,y,a,d,Z )
  proof
    consider u1,v1 be PartFunc of REAL,REAL such that
A48: u1=(Re f)* (R2-to-C) *<:x,y:> & v1=(Im f)* (R2-to-C) *<:x,y:> &
    integral(f,x,y,a,d,Z)
    = integral( u1(#)(x`|Z) - v1(#)(y`|Z) ,a,d )
    + integral( v1(#)(x`|Z) + u1(#)(y`|Z) ,a,d )*<i> by Def2;
    thus thesis by A5,A48;
  end;
A49: integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,d,b )
  + integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,d,b )*<i>
  = integral( f,x,y,d,b,Z )
  proof
    consider u1,v1 be PartFunc of REAL,REAL such that
A50: u1=(Re f)* (R2-to-C) *<:x,y:> & v1=(Im f)* (R2-to-C) *<:x,y:> &
    integral(f,x,y,d,b,Z)
    = integral( u1(#)(x`|Z) - v1(#)(y`|Z) ,d,b )
    + integral( v1(#)(x`|Z) + u1(#)(y`|Z) ,d,b )*<i> by Def2;
    thus thesis by A5,A50;
  end;
A51: integral( f,x,y,a,d,Z ) = integral( f,x1,y1,a,d,Z1 )
  proof
    reconsider Z3 = Z /\ Z1 as Subset of REAL;
    reconsider ZZ=Z, ZZ1= Z1, ZZ3= Z3 as Subset of R^1 by TOPMETR:24;
    ZZ is open & ZZ1 is open by A3,A6,BORSUK_5:62; then
    ZZ /\ ZZ1 is open by TOPS_1:38; then
A52: Z3 is open by BORSUK_5:62;
A53: [.a,d.] c= [.a,b.] by A2,XXREAL_1:34;then
A54: [.a,d.] c= dom x & [.a,d.] c= dom y by A3,A4,XBOOLE_1:1;
A55: x| [.a,d.] = x1| [.a,d.]
    proof
A56:  dom (x| [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:90
      .= [.a,d.] by A3,A4,A53,XBOOLE_1:1,XBOOLE_1:28
      .= (dom x1) /\ [.a,d.] by A6,A7,XBOOLE_1:28
      .= dom (x1| [.a,d.]) by RELAT_1:90;
      for x0 be set st x0 in dom (x| [.a,d.])
      holds (x| [.a,d.]).x0 = (x1| [.a,d.]).x0
      proof
        let x0 be set such that
A57:    x0 in dom (x| [.a,d.]);
A58:    dom (x| [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:90
        .= [.a,d.] by A53,A3,A4,XBOOLE_1:1,XBOOLE_1:28;
        [.a,d.] c= (dom x1) /\ dom y1 by A6,A7,XBOOLE_1:19;then
        x0 in (dom x1) /\ dom y1 by A57,A58; then
        x0 in (dom x1) /\ dom (<i>(#)y1) by VALUED_1:def 5;then
A59:    x0 in dom (x1+<i>(#)y1) by VALUED_1:def 1;
        [.a,d.] c= (dom x) /\ dom y by A54,XBOOLE_1:19;then
        x0 in (dom x) /\ dom y by A57,A58;then
        x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A60:    x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
        reconsider t = x0 as Element of REAL by A57;
A61:    C.t = C1.t by A1,A57,A58;
A62:    C.t = (x+<i>(#)y).t by A3,A4,A53,A57,A58,FUNCT_1:72;
A63:    C1.t = (x1+<i>(#)y1).t by A6,A7,A57,A58,FUNCT_1:72;
A64:    (x1+<i>(#)y1).t = x1.t+(<i>(#)y1).t by A59,VALUED_1:def 1
        .= x1.t+<i>*y1.t by VALUED_1:6;
A65:    (x+<i>(#)y).t = x.t+(<i>(#)y).t by A60,VALUED_1:def 1
        .= x.t+<i>*y.t by VALUED_1:6;
        thus (x| [.a,d.]).x0 = x.x0 by A57,FUNCT_1:70
        .= x1.x0 by A61,A62,A63,A64,A65,COMPLEX1:163
        .= (x1| [.a,d.]).x0 by A58,A57,FUNCT_1:72;
      end;
      hence thesis by A56,FUNCT_1:9;
    end;
A66: y| [.a,d.] = y1| [.a,d.]
    proof
A67:  dom (y| [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:90
      .= [.a,d.] by A3,A4,A53,XBOOLE_1:1,XBOOLE_1:28
      .= (dom y1) /\ [.a,d.] by A6,A7,XBOOLE_1:28
      .= dom (y1| [.a,d.]) by RELAT_1:90;
      for x0 be set st x0 in dom (y| [.a,d.])
      holds (y| [.a,d.]).x0 = (y1| [.a,d.]).x0
      proof
        let x0 be set such that
A68:    x0 in dom (y| [.a,d.]);
A69:    dom (y| [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:90
        .= [.a,d.] by A3,A4,A53,XBOOLE_1:1,XBOOLE_1:28;
        [.a,d.] c= (dom x1) /\ dom y1 by A6,A7,XBOOLE_1:19;then
        x0 in (dom x1) /\ dom y1 by A68,A69;then
        x0 in (dom x1) /\ dom (<i>(#)y1) by VALUED_1:def 5;then
A70:    x0 in dom (x1+<i>(#)y1) by VALUED_1:def 1;
        [.a,d.] c= (dom x) /\ dom y by A54,XBOOLE_1:19;then
        x0 in (dom x) /\ dom y by A68,A69;then
        x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A71:    x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
        reconsider t = x0 as Element of REAL by A68;
A72:    C.t = C1.t by A1,A68,A69;
A73:    C.t = (x+<i>(#)y).t by A3,A4,A53,A68,A69,FUNCT_1:72;
A74:    C1.t = (x1+<i>(#)y1).t by A6,A7,A68,A69,FUNCT_1:72;
A75:    (x1+<i>(#)y1).t = x1.t+(<i>(#)y1).t by A70,VALUED_1:def 1
        .= x1.t+<i>*y1.t by VALUED_1:6;
A76:    (x+<i>(#)y).t = x.t+(<i>(#)y).t by A71,VALUED_1:def 1
        .= x.t+<i>*y.t by VALUED_1:6;
        thus (y| [.a,d.]).x0 = y.x0 by A68,FUNCT_1:70
        .= y1.x0 by A72,A73,A74,A75,A76,COMPLEX1:163
        .= (y1| [.a,d.]).x0 by A69,A68,FUNCT_1:72;
      end;
      hence thesis by A67,FUNCT_1:9;
    end;
A77: [.a,d.] c= Z by A3,A4,A53,XBOOLE_1:1;then
A78: [.a,d.] c= Z3 by A6,A7,XBOOLE_1:19;
A79: rng ((x+<i>(#)y) | [.a,d.]) c= dom f
    proof
      for y0 be set st y0 in rng ((x+<i>(#)y) | [.a,d.])
      holds y0 in dom f
      proof
        let y0 be set such that
A80:    y0 in rng ((x+<i>(#)y) | [.a,d.]);
        consider x0 be set such that
A81:    x0 in dom ((x+<i>(#)y) | [.a,d.])
        & y0 = ((x+<i>(#)y) | [.a,d.]).x0 by A80,FUNCT_1:def 5;
A82:    x0 in (dom (x+<i>(#)y)) /\ [.a,d.] by A81,RELAT_1:90;
        (dom (x+<i>(#)y)) /\ [.a,d.] c= (dom (x+<i>(#)y)) /\ [.a,b.]
        by A2,XXREAL_1:34,XBOOLE_1:26;then
        x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by A82;then
A83:    x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:90; then
A84:    ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
        by FUNCT_1:12;
        ((x+<i>(#)y) | [.a,d.]).x0 = (x+<i>(#)y).x0 by A81,FUNCT_1:70
        .= ((x+<i>(#)y) | [.a,b.]).x0 by A83,FUNCT_1:70;
        hence thesis by A1,A3,A81,A84;
      end;
      hence thesis by TARSKI:def 3;
    end;
A85: rng ((x1+<i>(#)y1) | [.a,d.]) c= dom f
    proof
      for y0 be set st y0 in rng ((x1+<i>(#)y1) | [.a,d.])
      holds y0 in dom f
      proof
        let y0 be set such that
A86:    y0 in rng ((x1+<i>(#)y1) | [.a,d.]);
        consider x0 be set such that
A87:    x0 in dom ((x1+<i>(#)y1) | [.a,d.])
        & y0 = ((x1+<i>(#)y1) | [.a,d.]).x0 by A86,FUNCT_1:def 5;
        x0 in (dom (x1+<i>(#)y1)) /\ [.a,d.] by A87,RELAT_1:90;
        then
A88:    x0 in [.a,d.] by XBOOLE_0:def 4;then
A89:    x0 in [.a,b.] by A53;
        x0 in (dom x) /\ (dom y) by A3,A4,A89,XBOOLE_0:def 4;then
        x0 in ((dom x) /\ (dom y)) /\ [.a,b.] by A53,A88,XBOOLE_0:def 4;
        then
        x0 in ((dom x) /\ dom (<i>(#)y)) /\ [.a,b.] by VALUED_1:def 5;
        then
        x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by VALUED_1:def 1;then
        x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:90; then
A90:    ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
        by FUNCT_1:12;
        reconsider t = x0 as Element of REAL by A87;
A91:    C.t = (x+<i>(#)y).t by A3,A4,A53,A88,FUNCT_1:72;
A92:    C1.t = (x1+<i>(#)y1).t by A6,A7,A88,FUNCT_1:72;
        ((x1+<i>(#)y1) | [.a,d.]).x0
        = (x1+<i>(#)y1).x0 by A87,FUNCT_1:70
        .= (x+<i>(#)y).x0 by A1,A88,A91,A92
        .= ((x+<i>(#)y) | [.a,b.]).x0 by A53,A88,FUNCT_1:72;
        hence thesis by A1,A3,A87,A90;
      end;
      hence thesis by TARSKI:def 3;
    end;
A93: x is_differentiable_on Z3 &
    y is_differentiable_on Z3 by A3,A52,XBOOLE_1:17,FDIFF_1:34;
A94: x1 is_differentiable_on Z3 &
    y1 is_differentiable_on Z3 by A6,A52,XBOOLE_1:17,FDIFF_1:34;
A95: [.a,d.] c= dom x & [.a,d.] c= dom y by A3,A4,A53,XBOOLE_1:1;
    hence integral(f,x,y,a,d,Z)
    = integral(f,x,y,a,d,Z3) by A3,A6,A7,A52,A79,A78,Lm1,XBOOLE_1:17
    .= integral(f,x1,y1,a,d,Z3)
    by A6,A7,A52,A55,A66,A77,A79,A85,A93,A94,A95,Lm2,XBOOLE_1:19
    .= integral(f,x1,y1,a,d,Z1) by A6,A7,A52,A78,A85,Lm1,XBOOLE_1:17;
  end;
A96: integral( f,x,y,d,b,Z ) = integral( f,x2,y2,d,b,Z2 )
  proof
    reconsider Z3 = Z /\ Z2 as Subset of REAL;
    reconsider ZZ=Z, ZZ1= Z2, ZZ3= Z3 as Subset of R^1 by TOPMETR:24;
    ZZ is open & ZZ1 is open by A3,A12,BORSUK_5:62; then
    ZZ /\ ZZ1 is open by TOPS_1:38; then
A97: Z3 is open by BORSUK_5:62;
A98: [.d,b.] c= [.a,b.] by A2,XXREAL_1:34;then
A99: [.d,b.] c= dom x & [.d,b.] c= dom y by A3,A4,XBOOLE_1:1;
A100: x| [.d,b.] = x2| [.d,b.]
    proof
A101: dom (x| [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:90
      .= [.d,b.] by A3,A4,A98,XBOOLE_1:1,XBOOLE_1:28
      .= (dom x2) /\ [.d,b.] by A12,A13,XBOOLE_1:28
      .= dom (x2| [.d,b.]) by RELAT_1:90;
      for x0 be set st x0 in dom (x| [.d,b.])
      holds (x| [.d,b.]).x0 = (x2| [.d,b.]).x0
      proof
        let x0 be set such that
A102:   x0 in dom (x| [.d,b.]);
A103:   dom (x| [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:90
        .= [.d,b.] by A3,A4,A98,XBOOLE_1:1,XBOOLE_1:28;
        [.d,b.] c= (dom x2) /\ dom y2 by A12,A13,XBOOLE_1:19;then
        x0 in (dom x2) /\ dom y2 by A102,A103; then
        x0 in (dom x2) /\ dom (<i>(#)y2) by VALUED_1:def 5;then
A104:   x0 in dom (x2+<i>(#)y2) by VALUED_1:def 1;
        [.d,b.] c= (dom x) /\ dom y by A99,XBOOLE_1:19;then
        x0 in (dom x) /\ dom y by A102,A103; then
        x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A105:   x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
        reconsider t = x0 as Element of REAL by A102;
A106:   C.t = C2.t by A1,A102,A103;
A107:   C.t = (x+<i>(#)y).t by A3,A4,A98,A102,A103,FUNCT_1:72;
A108:   C2.t = (x2+<i>(#)y2).t by A12,A13,A102,A103,FUNCT_1:72;
A109:   (x2+<i>(#)y2).t = x2.t+(<i>(#)y2).t by A104,VALUED_1:def 1
        .= x2.t+<i>*y2.t by VALUED_1:6;
A110:   (x+<i>(#)y).t = x.t+(<i>(#)y).t by A105,VALUED_1:def 1
        .= x.t+<i>*y.t by VALUED_1:6;
        thus (x| [.d,b.]).x0 = x.x0 by A102,FUNCT_1:70
        .= x2.x0 by A106,A107,A108,A109,A110,COMPLEX1:163
        .= (x2| [.d,b.]).x0 by A102,A103,FUNCT_1:72;
      end;
      hence thesis by A101,FUNCT_1:9;
    end;
A111: y| [.d,b.] = y2| [.d,b.]
    proof
A112: dom (y| [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:90
      .= [.d,b.] by A3,A4,A98,XBOOLE_1:1,XBOOLE_1:28
      .= (dom y2) /\ [.d,b.] by A12,A13,XBOOLE_1:28
      .= dom (y2| [.d,b.]) by RELAT_1:90;
      for x0 be set st x0 in dom (y| [.d,b.])
      holds (y| [.d,b.]).x0 = (y2| [.d,b.]).x0
      proof
        let x0 be set such that
A113:   x0 in dom (y| [.d,b.]);
A114:   dom (y| [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:90
        .= [.d,b.] by A3,A4,A98,XBOOLE_1:1,XBOOLE_1:28;
        [.d,b.] c= (dom x2) /\ dom y2 by A12,A13,XBOOLE_1:19;then
        x0 in (dom x2) /\ dom y2 by A113,A114;then
        x0 in (dom x2) /\ dom (<i>(#)y2) by VALUED_1:def 5;then
A115:   x0 in dom (x2+<i>(#)y2) by VALUED_1:def 1;
        [.d,b.] c= (dom x) /\ dom y by A99,XBOOLE_1:19;then
        x0 in (dom x) /\ dom y by A113,A114;then
        x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A116:   x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
        reconsider t = x0 as Element of REAL by A113;
A117:   C.t = C2.t by A1,A113,A114;
A118:   C.t = (x+<i>(#)y).t by A3,A4,A98,A113,A114,FUNCT_1:72;
A119:   C2.t = (x2+<i>(#)y2).t by A12,A13,A113,A114,FUNCT_1:72;
A120:   (x2+<i>(#)y2).t = x2.t+(<i>(#)y2).t by A115,VALUED_1:def 1
        .= x2.t+<i>*y2.t by VALUED_1:6;
A121:   (x+<i>(#)y).t = x.t+(<i>(#)y).t by A116,VALUED_1:def 1
        .= x.t+<i>*y.t by VALUED_1:6;
        thus (y| [.d,b.]).x0 = y.x0 by A113,FUNCT_1:70
        .= y2.x0 by A117,A118,A119,A120,A121,COMPLEX1:163
        .= (y2| [.d,b.]).x0 by A114,A113,FUNCT_1:72;
      end;
      hence thesis by A112,FUNCT_1:9;
    end;
A122: [.d,b.] c= Z by A3,A4,A98,XBOOLE_1:1;then
A123: [.d,b.] c= Z3 by A12,A13,XBOOLE_1:19;
A124: rng ((x+<i>(#)y) | [.d,b.]) c= dom f
    proof
      for y0 be set st y0 in rng ((x+<i>(#)y) | [.d,b.])
      holds y0 in dom f
      proof
        let y0 be set such that
A125:   y0 in rng ((x+<i>(#)y) | [.d,b.]);
        consider x0 be set such that
A126:   x0 in dom ((x+<i>(#)y) | [.d,b.]) &
        y0 = ((x+<i>(#)y) | [.d,b.]).x0 by A125,FUNCT_1:def 5;
A127:   x0 in (dom (x+<i>(#)y)) /\ [.d,b.] by A126,RELAT_1:90;
        (dom (x+<i>(#)y)) /\ [.d,b.] c= (dom (x+<i>(#)y)) /\ [.a,b.]
        by A2,XXREAL_1:34,XBOOLE_1:26;then
        x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by A127;then
A128:   x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:90;then
A129:   ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
        by FUNCT_1:12;
        ((x+<i>(#)y) | [.d,b.]).x0 = (x+<i>(#)y).x0 by A126,FUNCT_1:70
        .= ((x+<i>(#)y) | [.a,b.]).x0 by A128,FUNCT_1:70;
        hence thesis by A1,A3,A126,A129;
      end;
      hence thesis by TARSKI:def 3;
    end;
A130: rng ((x2+<i>(#)y2) | [.d,b.]) c= dom f
    proof
      for y0 be set st y0 in rng ((x2+<i>(#)y2) | [.d,b.])
      holds y0 in dom f
      proof
        let y0 be set such that
A131:   y0 in rng ((x2+<i>(#)y2) | [.d,b.]);
        consider x0 be set such that
A132:   x0 in dom ((x2+<i>(#)y2) | [.d,b.]) &
        y0 = ((x2+<i>(#)y2) | [.d,b.]).x0 by A131,FUNCT_1:def 5;
        x0 in (dom (x2+<i>(#)y2)) /\ [.d,b.] by A132,RELAT_1:90;
        then
A133:   x0 in [.d,b.] by XBOOLE_0:def 4;then
A134:   x0 in [.a,b.] by A98;
        x0 in (dom x) /\ (dom y) by A3,A4,A134,XBOOLE_0:def 4;then
        x0 in ((dom x) /\ (dom y)) /\ [.a,b.] by A98,A133,XBOOLE_0:def 4;
        then
        x0 in ((dom x) /\ dom (<i>(#)y)) /\ [.a,b.] by VALUED_1:def 5;
        then
        x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by VALUED_1:def 1;then
        x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:90;then
A135:   ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
        by FUNCT_1:12;
        reconsider t = x0 as Element of REAL by A132;
A136:   C.t = (x+<i>(#)y).t by A3,A4,A98,A133,FUNCT_1:72;
A137:   C2.t = (x2+<i>(#)y2).t by A12,A13,A133,FUNCT_1:72;
        ((x2+<i>(#)y2) | [.d,b.]).x0
        = (x2+<i>(#)y2).x0 by A132,FUNCT_1:70
        .= (x+<i>(#)y).x0 by A1,A133,A136,A137
        .= ((x+<i>(#)y) | [.a,b.]).x0 by A98,A133,FUNCT_1:72;
        hence thesis by A1,A3,A132,A135;
      end;
      hence thesis by TARSKI:def 3;
    end;
A138: x is_differentiable_on Z3 &
    y is_differentiable_on Z3 by A3,A97,XBOOLE_1:17,FDIFF_1:34;
A139: x2 is_differentiable_on Z3 &
    y2 is_differentiable_on Z3 by A12,A97,XBOOLE_1:17,FDIFF_1:34;
A140: [.d,b.] c= dom x & [.d,b.] c= dom y by A3,A4,A98,XBOOLE_1:1;
    hence integral(f,x,y,d,b,Z) = integral(f,x,y,d,b,Z3)
    by A3,A12,A13,A97,A123,A124,Lm1,XBOOLE_1:17
    .= integral(f,x2,y2,d,b,Z3)
    by Lm2,A12,A13,A97,A100,A111,A122,A124,A130,A138,A139,A140,XBOOLE_1:19
    .= integral(f,x2,y2,d,b,Z2) by A12,A13,A97,A123,A130,Lm1,XBOOLE_1:17;
  end;
  thus integral(f,C) = integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
  + integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i> by A1,A3,A5,Def4
  .= integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,d )
  + integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,d,b )
  + integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i>
  by A1,A18,A39,A40,A41,INTEGRA6:17
  .= integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,d )
  + integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,d,b )
  +(integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,d )
  + integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,d,b ))*<i>
  by A1,A18,A39,A40,A44,INTEGRA6:17
  .= integral( f,x1,y1,a,d,Z1 ) + integral( f,x,y,d,b,Z ) by A51,A49,A47
  .= integral(f,C1) + integral(f,C2) by A6,A7,A8,A17,Def4,A96;
end;