let a, b be Real; :: thesis: for x1, y1, x2, y2 being PartFunc of REAL ,REAL
for Z being Subset of REAL
for f being PartFunc of COMPLEX ,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z
let x1, y1, x2, y2 be PartFunc of REAL ,REAL ; :: thesis: for Z being Subset of REAL
for f being PartFunc of COMPLEX ,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z
let Z be Subset of REAL ; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX st a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f holds
integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f implies integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z )
assume A1: ( a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 & [.a,b.] c= dom x2 & [.a,b.] c= dom y2 & x1 | [.a,b.] = x2 | [.a,b.] & y1 | [.a,b.] = y2 | [.a,b.] & Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z & rng ((x1 + (<i> (#) y1)) | [.a,b.]) c= dom f & x2 is_differentiable_on Z & y2 is_differentiable_on Z & rng ((x2 + (<i> (#) y2)) | [.a,b.]) c= dom f ) ; :: thesis: integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z
consider u01, v01 being PartFunc of REAL ,REAL such that
A2: ( u01 = ((Re f) * R2-to-C ) * <:x1,y1:> & v01 = ((Im f) * R2-to-C ) * <:x1,y1:> & integral f,x1,y1,a,b,Z = (integral ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b) + ((integral ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b) * <i> ) ) by Def2;
consider u02, v02 being PartFunc of REAL ,REAL such that
A3: ( u02 = ((Re f) * R2-to-C ) * <:x2,y2:> & v02 = ((Im f) * R2-to-C ) * <:x2,y2:> & integral f,x2,y2,a,b,Z = (integral ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) + ((integral ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b) * <i> ) ) by Def2;
reconsider AB = [.a,b.] as closed-interval Subset of REAL by A1, INTEGRA1:def 1;

A4: now

assume A5: ( not a = b & not a < b ) ; :: thesis: contradiction
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; :: thesis: verum

end;

per cases ( a < b or a = b ) by A4;

suppose A6: a < b ; :: thesis: integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z

A7: u01 | AB = u02 | AB

proof

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

proof

A9: for x0 being set st x0 in dom (u01 | AB) holds
x0 in dom (u02 | AB)

proof

let x0 be set ; :: thesis: ( x0 in dom (u01 | AB) implies x0 in dom (u02 | AB) )
assume A10: x0 in dom (u01 | AB) ; :: thesis: x0 in dom (u02 | AB)
x0 in (dom u01) /\ AB by A10, RELAT_1: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 x0 in dom (u02 | AB) by RELAT_1:90; :: thesis: verum

end;

for x0 being set st x0 in dom (u02 | AB) holds
x0 in dom (u01 | AB)

proof

let x0 be set ; :: thesis: ( x0 in dom (u02 | AB) implies x0 in dom (u01 | AB) )
assume A13: x0 in dom (u02 | AB) ; :: thesis: x0 in dom (u01 | AB)
x0 in (dom u02) /\ AB by A13, RELAT_1: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 x0 in dom (u01 | AB) by RELAT_1:90; :: thesis: verum

end;

hence dom (u01 | AB) = dom (u02 | AB) by A9, TARSKI:2; :: thesis: verum

end;

for x0 being set st x0 in dom (u01 | AB) holds
(u01 | AB) . x0 = (u02 | AB) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (u01 | AB) implies (u01 | AB) . x0 = (u02 | AB) . x0 )
assume A16: x0 in dom (u01 | AB) ; :: thesis: (u01 | AB) . x0 = (u02 | AB) . x0
x0 in (dom u01) /\ AB by A16, RELAT_1:90;
then A17: x0 in AB by XBOOLE_0:def 4;
reconsider x0 = 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 (u01 | AB) . x0 = (u02 | AB) . x0 by A17, A18, A19, A21, A22, A23, FUNCT_3:68; :: thesis: verum

end;

hence u01 | AB = u02 | AB by A8, FUNCT_1:def 17; :: thesis: verum

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

proof

let x0 be set ; :: thesis: ( x0 in dom ((x1 `| Z) | AB) implies ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0 )
assume A27: x0 in dom ((x1 `| Z) | AB) ; :: thesis: ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0
reconsider x0 = 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.[ & not x0 = a & not x0 = b ) ; :: thesis: contradiction
x0 in { r where r is Real : ( a <= r & r <= b ) } by A25, A27, RCOMP_1:def 1;
then A33: ex r being Real st
( r = x0 & a <= r & r <= b ) ;

A34: now

assume A35: ( not a = x0 & not a < x0 ) ; :: thesis: contradiction
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; :: thesis: verum

end;

A36: now

assume A37: ( not x0 = b & not x0 < b ) ; :: thesis: contradiction
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; :: thesis: verum

end;

not x0 in { q where q is Real : ( a < q & q < b ) } by A32, RCOMP_1:def 2;
hence contradiction by A32, A34, A36; :: thesis: verum

end;

diff x1,x0 = diff x2,x0

proof

per cases ( x0 = a or x0 in ].a,b.[ or x0 = b ) by A31;

suppose A39: x0 = a ; :: thesis: diff x1,x0 = diff x2,x0

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
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;
then A44: x1 - x2 is_right_differentiable_in x0 by A42, 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 being convergent_to_0 Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
let c1 be constant Real_Sequence; :: thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) implies lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 )
assume A46: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) ) ; :: thesis: lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A47: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A48: 0 < b - x0 by A6, A39, XREAL_1:52;
then consider n being Element of NAT such that
A49: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < (b - x0) / 2 by A47, SEQ_2:def 7;
A50: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1

proof

let p1 be real number ; :: thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1 )
assume A51: 0 < p1 ; :: thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1
for m being Element of NAT st n <= m holds
((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 )
assume A52: n <= m ; :: thesis: ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
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 being set st x in rng c1 holds
x in dom (x1 - x2) by A46, A59, TARSKI:def 1;
hence rng c1 c= dom (x1 - x2) by TARSKI:def 3; :: thesis: verum

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 ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A66, A67; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1 by A51, COMPLEX1:130; :: thesis: verum

end;

then (h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) is convergent by SEQ_2:def 6;
hence lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 by A50, SEQ_2:def 7; :: thesis: verum

end;

then (Rdiff x1,x0) - (Rdiff x2,x0) = 0 by A44, A45, FDIFF_3:def 6;
hence Rdiff x1,x0 = Rdiff x2,x0 ; :: thesis: verum

end;

hence diff x1,x0 = diff x2,x0 by A41, A43, FDIFF_3:22; :: thesis: verum

end;

suppose A68: x0 in ].a,b.[ ; :: thesis: diff x1,x0 = diff x2,x0

A69: ].a,b.[ is open by RCOMP_1:25;
A70: ].a,b.[ c= [.a,b.]

proof

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

proof

let x0 be set ; :: thesis: ( x0 in ].a,b.[ implies x0 in [.a,b.] )
assume A71: x0 in ].a,b.[ ; :: thesis: 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 being Element of REAL st
( r = x0 & a < r & r < b ) ;
then reconsider x0 = x0 as Real ;
x0 in { r where r is Real : ( a <= r & r <= b ) } by A72;
hence x0 in [.a,b.] by RCOMP_1:def 1; :: thesis: verum

end;

hence ].a,b.[ c= [.a,b.] by TARSKI:def 3; :: thesis: verum

end;

then 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 being set st x0 in dom (x1 | ].a,b.[) holds
(x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (x1 | ].a,b.[) implies (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0 )
assume A80: x0 in dom (x1 | ].a,b.[) ; :: thesis: (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0
A81: dom (x1 | ].a,b.[) = (dom x1) /\ ].a,b.[ by RELAT_1:90
.= ].a,b.[ by A1, A70, XBOOLE_1:1, XBOOLE_1:28 ;
then (x1 | ].a,b.[) . x0 = x1 . x0 by A80, 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 (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0 ; :: thesis: verum

end;

hence diff x1,x0 = diff x2,x0 by A74, A75, A77, A78, A79, FUNCT_1:9; :: thesis: verum

end;

suppose A82: x0 = b ; :: thesis: diff x1,x0 = diff x2,x0

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
then A83: x0 in [.a,b.] by RCOMP_1:def 1;
then A84: x1 is_differentiable_in x0 by A1, FDIFF_1: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;
then A87: x1 - x2 is_left_differentiable_in x0 by A85, FDIFF_3:11;
Ldiff x1,x0 = Ldiff x2,x0

proof

A88: (Ldiff x1,x0) - (Ldiff x2,x0) = Ldiff (x1 - x2),x0 by A85, A86, FDIFF_3:11;
for h being convergent_to_0 Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
let c1 be constant Real_Sequence; :: thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) implies lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 )
assume A89: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) ) ; :: thesis: lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A90: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A91: 0 < b - a by A6, XREAL_1:52;
then consider n being Element of NAT such that
A92: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < (x0 - a) / 2 by A82, A90, SEQ_2:def 7;
A93: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1

proof

let p1 be real number ; :: thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1 )
assume A94: 0 < p1 ; :: thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1
for m being Element of NAT st n <= m holds
((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 )
assume A95: n <= m ; :: thesis: ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
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 being set st x in rng c1 holds
x in dom (x1 - x2) by A89, A102, TARSKI:def 1;
hence rng c1 c= dom (x1 - x2) by TARSKI:def 3; :: thesis: verum

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 ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A108, A109; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0 ) < p1 by A94, COMPLEX1:130; :: thesis: verum

end;

then (h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) is convergent by SEQ_2:def 6;
hence lim ((h " ) (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0 by A93, SEQ_2:def 7; :: thesis: verum

end;

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

end;

hence diff x1,x0 = diff x2,x0 by A84, A86, FDIFF_3:22; :: thesis: verum

end;

end;

end;

hence ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0 by A25, A27, A28, A29, A30, FUNCT_1:72; :: thesis: verum

end;

hence (x1 `| Z) | AB = (x2 `| Z) | AB by A25, A26, FUNCT_1:def 17; :: thesis: verum

end;

A110: v01 | AB = v02 | AB

proof

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

proof

A112: for x0 being set st x0 in dom (v01 | AB) holds
x0 in dom (v02 | AB)

proof

let x0 be set ; :: thesis: ( x0 in dom (v01 | AB) implies x0 in dom (v02 | AB) )
assume A113: x0 in dom (v01 | AB) ; :: thesis: x0 in dom (v02 | 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 x0 in dom (v02 | AB) by RELAT_1:90; :: thesis: verum

end;

for x0 being set st x0 in dom (v02 | AB) holds
x0 in dom (v01 | AB)

proof

let x0 be set ; :: thesis: ( x0 in dom (v02 | AB) implies x0 in dom (v01 | AB) )
assume A116: x0 in dom (v02 | AB) ; :: thesis: x0 in dom (v01 | 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 x0 in dom (v01 | AB) by RELAT_1:90; :: thesis: verum

end;

hence dom (v01 | AB) = dom (v02 | AB) by A112, TARSKI:2; :: thesis: verum

end;

for x0 being set st x0 in dom (v01 | AB) holds
(v01 | AB) . x0 = (v02 | AB) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (v01 | AB) implies (v01 | AB) . x0 = (v02 | AB) . x0 )
assume A119: x0 in dom (v01 | AB) ; :: thesis: (v01 | AB) . x0 = (v02 | AB) . x0
x0 in (dom v01) /\ AB by A119, RELAT_1:90;
then A120: x0 in AB by XBOOLE_0:def 4;
reconsider x0 = 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 (v01 | AB) . x0 = (v02 | AB) . x0 by A125, A126, A122, A120, A121, FUNCT_3:68, A124; :: thesis: verum

end;

hence v01 | AB = v02 | AB by A111, FUNCT_1:def 17; :: thesis: verum

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 being set st x0 in dom ((y1 `| Z) | AB) holds
((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom ((y1 `| Z) | AB) implies ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0 )
assume A130: x0 in dom ((y1 `| Z) | AB) ; :: thesis: ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0
reconsider x0 = 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.[ & not x0 = a & not x0 = b ) ; :: thesis: contradiction
x0 in { r where r is Real : ( a <= r & r <= b ) } by A128, A130, RCOMP_1:def 1;
then A136: ex r being Real st
( r = x0 & a <= r & r <= b ) ;

A137: now

assume A138: ( not a = x0 & not a < x0 ) ; :: thesis: contradiction
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; :: thesis: verum

end;

A139: now

assume A140: ( not x0 = b & not x0 < b ) ; :: thesis: contradiction
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; :: thesis: verum

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

end;

diff y1,x0 = diff y2,x0

proof

per cases ( x0 = a or x0 in ].a,b.[ or x0 = b ) by A134;

suppose A142: x0 = a ; :: thesis: diff y1,x0 = diff y2,x0

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
then A143: x0 in [.a,b.] by RCOMP_1:def 1;
then A144: y1 is_differentiable_in x0 by A1, FDIFF_1: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;
then A147: y1 - y2 is_right_differentiable_in x0 by A145, FDIFF_3:17;
Rdiff y1,x0 = Rdiff y2,x0

proof

A148: (Rdiff y1,x0) - (Rdiff y2,x0) = Rdiff (y1 - y2),x0 by A145, A146, FDIFF_3:17;
for h being convergent_to_0 Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) holds
lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
let c1 be constant Real_Sequence; :: thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) implies lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 )
assume A149: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) ) ; :: thesis: lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A150: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A151: 0 < b - x0 by A6, A142, XREAL_1:52;
then consider n being Element of NAT such that
A152: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < (b - x0) / 2 by A150, SEQ_2:def 7;
A153: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1

proof

let p1 be real number ; :: thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1 )
assume A154: 0 < p1 ; :: thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1
for m being Element of NAT st n <= m holds
((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 )
assume A155: n <= m ; :: thesis: ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
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 being set st x in rng c1 holds
x in dom (y1 - y2) by A162, A149, TARSKI:def 1;
hence rng c1 c= dom (y1 - y2) by TARSKI:def 3; :: thesis: verum

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 ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A169, A170; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1 by A154, COMPLEX1:130; :: thesis: verum

end;

then (h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) is convergent by SEQ_2:def 6;
hence lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 by A153, SEQ_2:def 7; :: thesis: verum

end;

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

end;

hence diff y1,x0 = diff y2,x0 by A144, A146, FDIFF_3:22; :: thesis: verum

end;

suppose A171: x0 in ].a,b.[ ; :: thesis: diff y1,x0 = diff y2,x0

A172: ].a,b.[ is open by RCOMP_1:25;
A173: ].a,b.[ c= [.a,b.]

proof

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

proof

let x0 be set ; :: thesis: ( x0 in ].a,b.[ implies x0 in [.a,b.] )
assume A174: x0 in ].a,b.[ ; :: thesis: 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 being Element of REAL st
( r = x0 & a < r & r < b ) ;
then reconsider x0 = x0 as Real ;
x0 in { r where r is Real : ( a <= r & r <= b ) } by A175;
hence x0 in [.a,b.] by RCOMP_1:def 1; :: thesis: verum

end;

hence ].a,b.[ c= [.a,b.] by TARSKI:def 3; :: thesis: verum

end;

then 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 being set st x0 in dom (y1 | ].a,b.[) holds
(y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (y1 | ].a,b.[) implies (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0 )
assume A183: x0 in dom (y1 | ].a,b.[) ; :: thesis: (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0
A184: dom (y1 | ].a,b.[) = (dom y1) /\ ].a,b.[ by RELAT_1:90
.= ].a,b.[ by A1, A173, XBOOLE_1:1, XBOOLE_1:28 ;
then (y1 | ].a,b.[) . x0 = y1 . x0 by A183, 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 (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0 ; :: thesis: verum

end;

hence diff y1,x0 = diff y2,x0 by A177, A178, A180, A181, A182, FUNCT_1:9; :: thesis: verum

end;

suppose A185: x0 = b ; :: thesis: diff y1,x0 = diff y2,x0

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
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;
then A190: y1 - y2 is_left_differentiable_in x0 by A188, 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 being convergent_to_0 Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
let c1 be constant Real_Sequence; :: thesis: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) implies lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 )
assume A192: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) ) ; :: thesis: lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A193: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A194: 0 < b - a by A6, XREAL_1:52;
then consider n being Element of NAT such that
A195: for m being Element of NAT st n <= m holds
abs ((h . m) - 0 ) < (x0 - a) / 2 by A185, A193, SEQ_2:def 7;
A196: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1

proof

let p1 be real number ; :: thesis: ( 0 < p1 implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1 )
assume A197: 0 < p1 ; :: thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1
for m being Element of NAT st n <= m holds
((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 )
assume A198: n <= m ; :: thesis: ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
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 being set st x in rng c1 holds
x in dom (y1 - y2) by A192, A205, TARSKI:def 1;
hence rng c1 c= dom (y1 - y2) by TARSKI:def 3; :: thesis: verum

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 ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A211, A212; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0 ) < p1 by A197, COMPLEX1:130; :: thesis: verum

end;

then (h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) is convergent by SEQ_2:def 6;
hence lim ((h " ) (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 by A196, SEQ_2:def 7; :: thesis: verum

end;

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

end;

hence diff y1,x0 = diff y2,x0 by A187, A189, FDIFF_3:22; :: thesis: verum

end;

end;

end;

hence ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0 by A128, A130, A131, A132, A133, FUNCT_1:72; :: thesis: verum

end;

hence (y1 `| Z) | AB = (y2 `| Z) | AB by A128, A129, FUNCT_1:def 17; :: thesis: verum

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 ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB by A7, A24, A110, A127, A216; :: thesis: verum

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 ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB by A7, A24, A110, A127, A223; :: thesis: verum

end;

integral ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b = integral ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),AB by INTEGRA5:19
.= integral ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),AB by A220
.= integral ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b by INTEGRA5:19 ;
hence integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z by A2, A3, A219; :: thesis: verum

end;

suppose A227: a = b ; :: thesis: integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z

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;
integral ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b = integral ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),BA by A227, INTEGRA5:19;
then A233: integral ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b = - (integral ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) by INTEGRA5:20;
integral ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b = integral ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),AB by INTEGRA5:19;
then integral ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b = - (integral ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b) by A227, INTEGRA5:20;
hence integral f,x1,y1,a,b,Z = integral f,x2,y2,a,b,Z by A2, A3, A228, A229, A230, A231, A233; :: thesis: verum

end;

end;