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

A4: now

assume A5: ( not a = b & not a < b ) ; :: thesis: contradiction
then ( 0 < b - a or 0 < a - b ) by XREAL_1:55;
then ( a < a + (b - a) or 0 < a - b ) by XREAL_1:29;
then ( a < b or b < b + (a - b) ) by XREAL_1:29;
hence contradiction by A5, A1; :: thesis: verum

end;

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:61;
then A11: ( x0 in dom u01 & x0 in AB ) by XBOOLE_0:def 4;
then ( x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Re f) * R2-to-C) & x0 in AB ) by A2, FUNCT_1:11;
then ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_3:def 7;
then ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then ( x0 in AB & [((x2 | AB) . x0),((y2 | AB) . x0)] in dom ((Re f) * R2-to-C) ) by A1, FUNCT_1:49;
then ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then A12: ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
x0 in (dom x2) /\ (dom y2) by A1, A11, XBOOLE_0:def 4;
then x0 in dom <:x2,y2:> by FUNCT_3:def 7;
then ( x0 in AB & x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Re f) * R2-to-C) ) by A12, FUNCT_3:def 7;
then ( x0 in AB & x0 in dom u02 ) by A3, FUNCT_1:11;
then x0 in (dom u02) /\ AB by XBOOLE_0:def 4;
hence x0 in dom (u02 | AB) by RELAT_1:61; :: thesis: verum

end;

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

proof

let x0 be set ; :: thesis: ( x0 in dom (u02 | AB) implies x0 in dom (u01 | AB) )
assume A13: x0 in dom (u02 | AB) ; :: thesis: x0 in dom (u01 | AB)
x0 in (dom u02) /\ AB by A13, RELAT_1:61;
then A14: ( x0 in dom u02 & x0 in AB ) by XBOOLE_0:def 4;
then ( x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Re f) * R2-to-C) & x0 in AB ) by A3, FUNCT_1:11;
then ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_3:def 7;
then ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then ( x0 in AB & [((x1 | AB) . x0),((y1 | AB) . x0)] in dom ((Re f) * R2-to-C) ) by A1, FUNCT_1:49;
then ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
then A15: ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Re f) * R2-to-C) ) by FUNCT_1:49;
x0 in (dom x1) /\ (dom y1) by A1, A14, XBOOLE_0:def 4;
then x0 in dom <:x1,y1:> by FUNCT_3:def 7;
then ( x0 in AB & x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Re f) * R2-to-C) ) by A15, FUNCT_3:def 7;
then ( x0 in AB & x0 in dom u01 ) by A2, FUNCT_1:11;
then x0 in (dom u01) /\ AB by XBOOLE_0:def 4;
hence x0 in dom (u01 | AB) by RELAT_1:61; :: thesis: verum

end;

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

end;

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

proof

let x0 be set ; :: thesis: ( x0 in dom (u01 | AB) implies (u01 | AB) . x0 = (u02 | AB) . x0 )
assume A16: x0 in dom (u01 | AB) ; :: thesis: (u01 | AB) . x0 = (u02 | AB) . x0
x0 in (dom u01) /\ AB by A16, RELAT_1:61;
then A17: ( x0 in AB & x0 in dom u01 ) by XBOOLE_0:def 4;
then reconsider x0 = x0 as Real 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 7;
then A19: u01 . x0 = ((Re f) * R2-to-C) . (<:x1,y1:> . x0) by A2, FUNCT_1:13;
A20: AB c= (dom x2) /\ (dom y2) by A1, XBOOLE_1:19;
then x0 in (dom x2) /\ (dom y2) by A17;
then x0 in dom <:x2,y2:> by FUNCT_3:def 7;
then u02 . x0 = ((Re f) * R2-to-C) . (<:x2,y2:> . x0) by A3, FUNCT_1:13;
then A21: u02 . x0 = ((Re f) * R2-to-C) . [(x2 . x0),(y2 . x0)] by A17, A20, FUNCT_3:48;
A22: x1 . x0 = (x1 | [.a,b.]) . x0 by A17, FUNCT_1:49
.= x2 . x0 by A17, A1, FUNCT_1:49 ;
A23: y1 . x0 = (y1 | [.a,b.]) . x0 by A17, FUNCT_1:49
.= y2 . x0 by A17, A1, FUNCT_1:49 ;
( u01 . x0 = (u01 | AB) . x0 & u02 . x0 = (u02 | AB) . x0 ) by A17, FUNCT_1:49;
hence (u01 | AB) . x0 = (u02 | AB) . x0 by A17, A18, A19, A21, A22, A23, FUNCT_3:48; :: thesis: verum

end;

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

end;

A24: (x1 `| Z) | AB = (x2 `| Z) | AB

proof

A25: dom ((x1 `| Z) | AB) = (dom (x1 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def 7
.= AB by A1, XBOOLE_1:28 ;
A26: dom ((x2 `| Z) | AB) = (dom (x2 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def 7
.= AB by A1, XBOOLE_1:28 ;
for x0 being set st x0 in dom ((x1 `| Z) | AB) holds
((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom ((x1 `| Z) | AB) implies ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0 )
assume A27: x0 in dom ((x1 `| Z) | AB) ; :: thesis: ((x1 `| Z) | AB) . x0 = ((x2 `| Z) | AB) . x0
x0 in dom (x1 `| Z) by A27, RELAT_1:57;
then reconsider x0 = x0 as Real by A27;
A28: ((x2 `| Z) | AB) . x0 = (x2 `| Z) . x0 by A25, A27, FUNCT_1:49;
A29: (x1 `| Z) . x0 = diff (x1,x0) by A1, A25, A27, FDIFF_1:def 7;
A30: (x2 `| Z) . x0 = diff (x2,x0) by A1, A25, A27, FDIFF_1:def 7;

A31: now

assume A32: ( not x0 in ].a,b.[ & 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:55;
then ( a < a + (x0 - a) or 0 < a - x0 ) by XREAL_1:29;
then ( a < x0 or x0 < x0 + (a - x0) ) by XREAL_1:29;
hence contradiction by A33, A35; :: thesis: verum

end;

A36: now

assume A37: ( not x0 = b & not x0 < b ) ; :: thesis: contradiction
then ( 0 < x0 - b or 0 < b - x0 ) by XREAL_1:55;
then ( b < b + (x0 - b) or 0 < b - x0 ) by XREAL_1:29;
then ( b < x0 or x0 < x0 + (b - x0) ) by XREAL_1:29;
hence contradiction by A33, A37; :: thesis: verum

end;

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

end;

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

proof

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

suppose A38: x0 = a ; :: thesis: diff (x1,x0) = diff (x2,x0)

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
then A39: x0 in [.a,b.] by RCOMP_1:def 1;
then A40: x1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A41: ( x1 is_right_differentiable_in x0 & diff (x1,x0) = Rdiff (x1,x0) ) by FDIFF_3:22;
x2 is_differentiable_in x0 by A1, A39, FDIFF_1:9;
then A42: ( x2 is_right_differentiable_in x0 & diff (x2,x0) = Rdiff (x2,x0) ) by FDIFF_3:22;
then A43: x1 - x2 is_right_differentiable_in x0 by A41, FDIFF_3:17;
Rdiff (x1,x0) = Rdiff (x2,x0)

proof

A44: (Rdiff (x1,x0)) - (Rdiff (x2,x0)) = Rdiff ((x1 - x2),x0) by A41, A42, FDIFF_3:17;
for h being 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 A45: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n > 0 ) ) ; :: thesis: lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A46: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A47: 0 < b - x0 by A6, A38, XREAL_1:50;
then consider n being Element of NAT such that
A48: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (b - x0) / 2 by A46, SEQ_2:def 7;
A49: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1

proof

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

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 )
assume A51: n <= m ; :: thesis: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
A52: abs ((h . m) - 0) < (b - x0) / 2 by A48, A51;
A53: 0 < h . m by A45;
then A54: h . m < (b - x0) / 2 by A52, ABSVALUE:def 1;
A55: a + 0 <= x0 + (h . m) by A38, A53, XREAL_1:7;
x0 + (h . m) <= x0 + ((b - x0) / 2) by A54, XREAL_1:7;
then A56: (x0 + (h . m)) + 0 <= (b - ((b - x0) / 2)) + ((b - x0) / 2) by A47, XREAL_1:7;
A57: [.a,b.] c= (dom x1) /\ (dom x2) by A1, XBOOLE_1:19;
then x0 in (dom x1) /\ (dom x2) by A39;
then A58: x0 in dom (x1 - x2) by VALUED_1:12;
A59: [.a,b.] c= dom (x1 - x2) by A57, VALUED_1:12;
x0 + (h . m) in { r where r is Real : ( a <= r & r <= b ) } by A55, A56;
then A60: x0 + (h . m) in [.a,b.] by RCOMP_1:def 1;
A61: x0 in rng c1 by A45, TARSKI:def 1;
A62: lim c1 = c1 . m by SEQ_4:26;
A63: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A61, A62, SEQ_4:25 ;
A64: rng c1 c= dom (x1 - x2)

proof

for x being set st x in rng c1 holds
x in dom (x1 - x2) by A45, A58, TARSKI:def 1;
hence rng c1 c= dom (x1 - x2) by TARSKI:def 3; :: thesis: verum

end;

A65: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = ((h ") . m) * ((((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((x1 - x2) /* (h + c1)) . m) - (((x1 - x2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - (((x1 - x2) /* c1) . m)) by A45, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m))) by A64, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0)) by A61, A62, A63, SEQ_4:25 ;
A66: (x1 - x2) . ((h . m) + x0) = (x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A59, A60, VALUED_1:13
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A60, FUNCT_1:49
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - ((x2 | [.a,b.]) . ((h . m) + x0)) by A60, FUNCT_1:49
.= 0 by A1 ;
(x1 - x2) . x0 = (x1 . x0) - (x2 . x0) by A58, VALUED_1:13
.= ((x1 | [.a,b.]) . x0) - (x2 . x0) by A39, FUNCT_1:49
.= ((x1 | [.a,b.]) . x0) - ((x2 | [.a,b.]) . x0) by A39, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A65, A66; :: thesis: verum

end;

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

end;

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

end;

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

end;

hence diff (x1,x0) = diff (x2,x0) by A40, A42, FDIFF_3:22; :: thesis: verum

end;

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

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

proof

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

proof

let x0 be set ; :: thesis: ( x0 in ].a,b.[ implies x0 in [.a,b.] )
assume A70: x0 in ].a,b.[ ; :: thesis: x0 in [.a,b.]
x0 in { r where r is Real : ( a < r & r < b ) } by A70, RCOMP_1:def 2;
then A71: ex r being Element of REAL st
( r = x0 & a < r & r < b ) ;
then reconsider x0 = x0 as Real ;
x0 in { r where r is Real : ( a <= r & r <= b ) } by A71;
hence x0 in [.a,b.] by RCOMP_1:def 1; :: thesis: verum

end;

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

end;

then A72: x1 is_differentiable_on ].a,b.[ by A1, A68, FDIFF_1:26, XBOOLE_1:1;
then A73: ( x1 | ].a,b.[ is_differentiable_on ].a,b.[ & (x1 | ].a,b.[) `| ].a,b.[ = x1 `| ].a,b.[ ) by A68, FDIFF_2:16;
A74: (x1 `| ].a,b.[) . x0 = diff (x1,x0) by A67, A72, FDIFF_1:def 7;
A75: x2 is_differentiable_on ].a,b.[ by A68, A69, A1, FDIFF_1:26, XBOOLE_1:1;
then A76: ( x2 | ].a,b.[ is_differentiable_on ].a,b.[ & (x2 | ].a,b.[) `| ].a,b.[ = x2 `| ].a,b.[ ) by A68, FDIFF_2:16;
A77: (x2 `| ].a,b.[) . x0 = diff (x2,x0) by A67, A75, FDIFF_1:def 7;
A78: dom (x1 | ].a,b.[) = (dom x1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A69, XBOOLE_1:1, XBOOLE_1:28
.= (dom x2) /\ ].a,b.[ by A1, A69, XBOOLE_1:1, XBOOLE_1:28
.= dom (x2 | ].a,b.[) by RELAT_1:61 ;
for x0 being set st x0 in dom (x1 | ].a,b.[) holds
(x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (x1 | ].a,b.[) implies (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0 )
assume A79: x0 in dom (x1 | ].a,b.[) ; :: thesis: (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0
A80: dom (x1 | ].a,b.[) = (dom x1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A69, XBOOLE_1:1, XBOOLE_1:28 ;
then (x1 | ].a,b.[) . x0 = x1 . x0 by A79, FUNCT_1:49
.= (x1 | [.a,b.]) . x0 by A69, A79, A80, FUNCT_1:49
.= x2 . x0 by A69, A79, A80, A1, FUNCT_1:49
.= (x2 | ].a,b.[) . x0 by A79, A80, FUNCT_1:49 ;
hence (x1 | ].a,b.[) . x0 = (x2 | ].a,b.[) . x0 ; :: thesis: verum

end;

hence diff (x1,x0) = diff (x2,x0) by A73, A74, A76, A77, A78, FUNCT_1:2; :: thesis: verum

end;

suppose A81: x0 = b ; :: thesis: diff (x1,x0) = diff (x2,x0)

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
then A82: x0 in [.a,b.] by RCOMP_1:def 1;
then A83: x1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A84: ( x1 is_left_differentiable_in x0 & diff (x1,x0) = Ldiff (x1,x0) ) by FDIFF_3:22;
x2 is_differentiable_in x0 by A1, A82, FDIFF_1:9;
then A85: ( x2 is_left_differentiable_in x0 & diff (x2,x0) = Ldiff (x2,x0) ) by FDIFF_3:22;
then A86: x1 - x2 is_left_differentiable_in x0 by A84, FDIFF_3:11;
Ldiff (x1,x0) = Ldiff (x2,x0)

proof

A87: (Ldiff (x1,x0)) - (Ldiff (x2,x0)) = Ldiff ((x1 - x2),x0) by A84, A85, FDIFF_3:11;
for h being 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 A88: ( rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Element of NAT holds h . n < 0 ) ) ; :: thesis: lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A89: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A90: 0 < b - a by A6, XREAL_1:50;
then consider n being Element of NAT such that
A91: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (x0 - a) / 2 by A81, A89, SEQ_2:def 7;
A92: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0) < p1

proof

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

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 )
assume A94: n <= m ; :: thesis: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0
A95: abs ((h . m) - 0) < (x0 - a) / 2 by A91, A94;
A96: h . m < 0 by A88;
then A97: - (h . m) < (x0 - a) / 2 by A95, ABSVALUE:def 1;
A98: x0 + (h . m) <= b + 0 by A81, A96, XREAL_1:7;
x0 - ((x0 - a) / 2) <= x0 - (- (h . m)) by A97, XREAL_1:13;
then A99: (a + ((x0 - a) / 2)) - ((x0 - a) / 2) <= (x0 + (h . m)) - 0 by A81, A90, XREAL_1:13;
A100: [.a,b.] c= (dom x1) /\ (dom x2) by A1, XBOOLE_1:19;
then x0 in (dom x1) /\ (dom x2) by A82;
then A101: x0 in dom (x1 - x2) by VALUED_1:12;
A102: [.a,b.] c= dom (x1 - x2) by A100, VALUED_1:12;
x0 + (h . m) in { r where r is Real : ( a <= r & r <= b ) } by A98, A99;
then A103: x0 + (h . m) in [.a,b.] by RCOMP_1:def 1;
x0 in rng c1 by A88, TARSKI:def 1;
then A104: lim c1 = x0 by SEQ_4:25;
A105: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A104, SEQ_4:26 ;
A106: rng c1 c= dom (x1 - x2)

proof

for x being set st x in rng c1 holds
x in dom (x1 - x2) by A88, A101, TARSKI:def 1;
hence rng c1 c= dom (x1 - x2) by TARSKI:def 3; :: thesis: verum

end;

A107: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = ((h ") . m) * ((((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((x1 - x2) /* (h + c1)) . m) - (((x1 - x2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - (((x1 - x2) /* c1) . m)) by A88, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m))) by A106, FUNCT_2:108
.= ((h ") . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0)) by A104, A105, SEQ_4:26 ;
A108: (x1 - x2) . ((h . m) + x0) = (x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A102, A103, VALUED_1:13
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A103, FUNCT_1:49
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - ((x2 | [.a,b.]) . ((h . m) + x0)) by A103, FUNCT_1:49
.= 0 by A1 ;
(x1 - x2) . x0 = (x1 . x0) - (x2 . x0) by A101, VALUED_1:13
.= ((x1 | [.a,b.]) . x0) - (x2 . x0) by A82, FUNCT_1:49
.= ((x1 | [.a,b.]) . x0) - ((x2 | [.a,b.]) . x0) by A82, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A107, A108; :: thesis: verum

end;

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

end;

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

end;

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

end;

hence diff (x1,x0) = diff (x2,x0) by A83, A85, FDIFF_3:22; :: thesis: verum

end;

end;

end;

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

end;

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

end;

A109: v01 | AB = v02 | AB

proof

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

proof

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

proof

let x0 be set ; :: thesis: ( x0 in dom (v01 | AB) implies x0 in dom (v02 | AB) )
assume A112: x0 in dom (v01 | AB) ; :: thesis: x0 in dom (v02 | AB)
x0 in (dom v01) /\ AB by A112, RELAT_1:61;
then A113: ( x0 in dom v01 & x0 in AB ) by XBOOLE_0:def 4;
then ( x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Im f) * R2-to-C) & x0 in AB ) by A2, FUNCT_1:11;
then ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_3:def 7;
then ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then ( x0 in AB & [((x2 | AB) . x0),((y2 | AB) . x0)] in dom ((Im f) * R2-to-C) ) by A1, FUNCT_1:49;
then ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then A114: ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
x0 in (dom x2) /\ (dom y2) by A1, A113, XBOOLE_0:def 4;
then x0 in dom <:x2,y2:> by FUNCT_3:def 7;
then ( x0 in AB & x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Im f) * R2-to-C) ) by A114, FUNCT_3:def 7;
then ( x0 in AB & x0 in dom v02 ) by A3, FUNCT_1:11;
then x0 in (dom v02) /\ AB by XBOOLE_0:def 4;
hence x0 in dom (v02 | AB) by RELAT_1:61; :: thesis: verum

end;

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

proof

let x0 be set ; :: thesis: ( x0 in dom (v02 | AB) implies x0 in dom (v01 | AB) )
assume A115: x0 in dom (v02 | AB) ; :: thesis: x0 in dom (v01 | AB)
x0 in (dom v02) /\ AB by A115, RELAT_1:61;
then A116: ( x0 in dom v02 & x0 in AB ) by XBOOLE_0:def 4;
then ( x0 in dom <:x2,y2:> & <:x2,y2:> . x0 in dom ((Im f) * R2-to-C) & x0 in AB ) by A3, FUNCT_1:11;
then ( x0 in AB & [(x2 . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_3:def 7;
then ( x0 in AB & [((x2 | AB) . x0),(y2 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then ( x0 in AB & [((x1 | AB) . x0),((y1 | AB) . x0)] in dom ((Im f) * R2-to-C) ) by A1, FUNCT_1:49;
then ( x0 in AB & [((x1 | AB) . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
then A117: ( x0 in AB & [(x1 . x0),(y1 . x0)] in dom ((Im f) * R2-to-C) ) by FUNCT_1:49;
x0 in (dom x1) /\ (dom y1) by A1, A116, XBOOLE_0:def 4;
then x0 in dom <:x1,y1:> by FUNCT_3:def 7;
then ( x0 in AB & x0 in dom <:x1,y1:> & <:x1,y1:> . x0 in dom ((Im f) * R2-to-C) ) by A117, FUNCT_3:def 7;
then ( x0 in AB & x0 in dom v01 ) by A2, FUNCT_1:11;
then x0 in (dom v01) /\ AB by XBOOLE_0:def 4;
hence x0 in dom (v01 | AB) by RELAT_1:61; :: thesis: verum

end;

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

end;

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

proof

let x0 be set ; :: thesis: ( x0 in dom (v01 | AB) implies (v01 | AB) . x0 = (v02 | AB) . x0 )
assume A118: x0 in dom (v01 | AB) ; :: thesis: (v01 | AB) . x0 = (v02 | AB) . x0
x0 in (dom v01) /\ AB by A118, RELAT_1:61;
then A119: ( x0 in AB & x0 in dom v01 ) by XBOOLE_0:def 4;
then reconsider x0 = x0 as Real by A118;
A120: AB c= (dom x1) /\ (dom y1) by A1, XBOOLE_1:19;
then x0 in (dom x1) /\ (dom y1) by A119;
then x0 in dom <:x1,y1:> by FUNCT_3:def 7;
then A121: v01 . x0 = ((Im f) * R2-to-C) . (<:x1,y1:> . x0) by A2, FUNCT_1:13;
A122: AB c= (dom x2) /\ (dom y2) by A1, XBOOLE_1:19;
then x0 in (dom x2) /\ (dom y2) by A119;
then x0 in dom <:x2,y2:> by FUNCT_3:def 7;
then v02 . x0 = ((Im f) * R2-to-C) . (<:x2,y2:> . x0) by A3, FUNCT_1:13;
then A123: v02 . x0 = ((Im f) * R2-to-C) . [(x2 . x0),(y2 . x0)] by A119, A122, FUNCT_3:48;
A124: x1 . x0 = (x1 | [.a,b.]) . x0 by A119, FUNCT_1:49
.= x2 . x0 by A119, A1, FUNCT_1:49 ;
A125: y1 . x0 = (y1 | [.a,b.]) . x0 by A119, FUNCT_1:49
.= y2 . x0 by A119, A1, FUNCT_1:49 ;
( v01 . x0 = (v01 | AB) . x0 & v02 . x0 = (v02 | AB) . x0 ) by A119, FUNCT_1:49;
hence (v01 | AB) . x0 = (v02 | AB) . x0 by A124, A125, A121, A119, A120, A123, FUNCT_3:48; :: thesis: verum

end;

hence v01 | AB = v02 | AB by A110, FUNCT_1:def 11; :: thesis: verum

end;

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

proof

A127: dom ((y1 `| Z) | AB) = (dom (y1 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def 7
.= AB by A1, XBOOLE_1:28 ;
A128: dom ((y2 `| Z) | AB) = (dom (y2 `| Z)) /\ AB by RELAT_1:61
.= Z /\ AB by A1, FDIFF_1:def 7
.= AB by A1, XBOOLE_1:28 ;
for x0 being set st x0 in dom ((y1 `| Z) | AB) holds
((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom ((y1 `| Z) | AB) implies ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0 )
assume A129: x0 in dom ((y1 `| Z) | AB) ; :: thesis: ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0
x0 in dom (y1 `| Z) by A129, RELAT_1:57;
then reconsider x0 = x0 as Real by A129;
A130: ((y2 `| Z) | AB) . x0 = (y2 `| Z) . x0 by A127, A129, FUNCT_1:49;
A131: (y1 `| Z) . x0 = diff (y1,x0) by A1, A129, A127, FDIFF_1:def 7;
A132: (y2 `| Z) . x0 = diff (y2,x0) by A1, A129, A127, FDIFF_1:def 7;

A133: now

assume A134: ( not x0 in ].a,b.[ & not x0 = a & not x0 = b ) ; :: thesis: contradiction
x0 in { r where r is Real : ( a <= r & r <= b ) } by A127, A129, RCOMP_1:def 1;
then A135: ex r being Real st
( r = x0 & a <= r & r <= b ) ;

A136: now

assume A137: ( not a = x0 & not a < x0 ) ; :: thesis: contradiction
then ( 0 < x0 - a or 0 < a - x0 ) by XREAL_1:55;
then ( a < a + (x0 - a) or 0 < a - x0 ) by XREAL_1:29;
then ( a < x0 or x0 < x0 + (a - x0) ) by XREAL_1:29;
hence contradiction by A135, A137; :: thesis: verum

end;

A138: now

assume A139: ( not x0 = b & not x0 < b ) ; :: thesis: contradiction
then ( 0 < x0 - b or 0 < b - x0 ) by XREAL_1:55;
then ( b < b + (x0 - b) or 0 < b - x0 ) by XREAL_1:29;
then ( b < x0 or x0 < x0 + (b - x0) ) by XREAL_1:29;
hence contradiction by A135, A139; :: thesis: verum

end;

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

end;

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

proof

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

suppose A140: x0 = a ; :: thesis: diff (y1,x0) = diff (y2,x0)

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
then A141: x0 in [.a,b.] by RCOMP_1:def 1;
then A142: y1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A143: ( y1 is_right_differentiable_in x0 & diff (y1,x0) = Rdiff (y1,x0) ) by FDIFF_3:22;
y2 is_differentiable_in x0 by A1, A141, FDIFF_1:9;
then A144: ( y2 is_right_differentiable_in x0 & diff (y2,x0) = Rdiff (y2,x0) ) by FDIFF_3:22;
then A145: y1 - y2 is_right_differentiable_in x0 by A143, FDIFF_3:17;
Rdiff (y1,x0) = Rdiff (y2,x0)

proof

A146: (Rdiff (y1,x0)) - (Rdiff (y2,x0)) = Rdiff ((y1 - y2),x0) by A143, A144, FDIFF_3:17;
for h being 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 A147: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n > 0 ) ) ; :: thesis: lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A148: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A149: 0 < b - x0 by A6, A140, XREAL_1:50;
then consider n being Element of NAT such that
A150: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (b - x0) / 2 by A148, SEQ_2:def 7;
A151: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1

proof

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

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 )
assume A153: n <= m ; :: thesis: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
A154: abs ((h . m) - 0) < (b - x0) / 2 by A150, A153;
A155: 0 < h . m by A147;
then A156: h . m < (b - x0) / 2 by A154, ABSVALUE:def 1;
A157: a + 0 <= x0 + (h . m) by A140, A155, XREAL_1:7;
x0 + (h . m) <= x0 + ((b - x0) / 2) by A156, XREAL_1:7;
then A158: (x0 + (h . m)) + 0 <= (b - ((b - x0) / 2)) + ((b - x0) / 2) by A149, XREAL_1:7;
A159: [.a,b.] c= (dom y1) /\ (dom y2) by A1, XBOOLE_1:19;
then x0 in (dom y1) /\ (dom y2) by A141;
then A160: x0 in dom (y1 - y2) by VALUED_1:12;
A161: [.a,b.] c= dom (y1 - y2) by A159, VALUED_1:12;
x0 + (h . m) in { r where r is Real : ( a <= r & r <= b ) } by A157, A158;
then A162: x0 + (h . m) in [.a,b.] by RCOMP_1:def 1;
A163: x0 in rng c1 by A147, TARSKI:def 1;
A164: lim c1 = c1 . m by SEQ_4:26;
A165: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A164, A163, SEQ_4:25 ;
A166: rng c1 c= dom (y1 - y2)

proof

for x being set st x in rng c1 holds
x in dom (y1 - y2) by A160, A147, TARSKI:def 1;
hence rng c1 c= dom (y1 - y2) by TARSKI:def 3; :: thesis: verum

end;

A167: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = ((h ") . m) * ((((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((y1 - y2) /* (h + c1)) . m) - (((y1 - y2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - (((y1 - y2) /* c1) . m)) by A147, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m))) by A166, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0)) by A163, A164, A165, SEQ_4:25 ;
A168: (y1 - y2) . ((h . m) + x0) = (y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A161, A162, VALUED_1:13
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A162, FUNCT_1:49
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - ((y2 | [.a,b.]) . ((h . m) + x0)) by A162, FUNCT_1:49
.= 0 by A1 ;
(y1 - y2) . x0 = (y1 . x0) - (y2 . x0) by A160, VALUED_1:13
.= ((y1 | [.a,b.]) . x0) - (y2 . x0) by A141, FUNCT_1:49
.= ((y1 | [.a,b.]) . x0) - ((y2 | [.a,b.]) . x0) by A141, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A167, A168; :: thesis: verum

end;

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

end;

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

end;

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

end;

hence diff (y1,x0) = diff (y2,x0) by A142, A144, FDIFF_3:22; :: thesis: verum

end;

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

A170: ].a,b.[ is open by RCOMP_1:7;
A171: ].a,b.[ c= [.a,b.]

proof

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

proof

let x0 be set ; :: thesis: ( x0 in ].a,b.[ implies x0 in [.a,b.] )
assume A172: x0 in ].a,b.[ ; :: thesis: x0 in [.a,b.]
x0 in { r where r is Real : ( a < r & r < b ) } by A172, RCOMP_1:def 2;
then A173: ex r being Element of REAL st
( r = x0 & a < r & r < b ) ;
then reconsider x0 = x0 as Real ;
x0 in { r where r is Real : ( a <= r & r <= b ) } by A173;
hence x0 in [.a,b.] by RCOMP_1:def 1; :: thesis: verum

end;

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

end;

then A174: y1 is_differentiable_on ].a,b.[ by A1, A170, FDIFF_1:26, XBOOLE_1:1;
then A175: ( y1 | ].a,b.[ is_differentiable_on ].a,b.[ & (y1 | ].a,b.[) `| ].a,b.[ = y1 `| ].a,b.[ ) by A170, FDIFF_2:16;
A176: (y1 `| ].a,b.[) . x0 = diff (y1,x0) by A169, A174, FDIFF_1:def 7;
A177: y2 is_differentiable_on ].a,b.[ by A1, A170, A171, FDIFF_1:26, XBOOLE_1:1;
then A178: ( y2 | ].a,b.[ is_differentiable_on ].a,b.[ & (y2 | ].a,b.[) `| ].a,b.[ = y2 `| ].a,b.[ ) by A170, FDIFF_2:16;
A179: (y2 `| ].a,b.[) . x0 = diff (y2,x0) by A169, A177, FDIFF_1:def 7;
A180: dom (y1 | ].a,b.[) = (dom y1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A171, XBOOLE_1:1, XBOOLE_1:28
.= (dom y2) /\ ].a,b.[ by A1, A171, XBOOLE_1:1, XBOOLE_1:28
.= dom (y2 | ].a,b.[) by RELAT_1:61 ;
for x0 being set st x0 in dom (y1 | ].a,b.[) holds
(y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0

proof

let x0 be set ; :: thesis: ( x0 in dom (y1 | ].a,b.[) implies (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0 )
assume A181: x0 in dom (y1 | ].a,b.[) ; :: thesis: (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0
A182: dom (y1 | ].a,b.[) = (dom y1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A171, XBOOLE_1:1, XBOOLE_1:28 ;
then (y1 | ].a,b.[) . x0 = y1 . x0 by A181, FUNCT_1:49
.= (y1 | [.a,b.]) . x0 by A171, A181, A182, FUNCT_1:49
.= y2 . x0 by A171, A181, A182, A1, FUNCT_1:49
.= (y2 | ].a,b.[) . x0 by A181, A182, FUNCT_1:49 ;
hence (y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0 ; :: thesis: verum

end;

hence diff (y1,x0) = diff (y2,x0) by A175, A176, A178, A179, A180, FUNCT_1:2; :: thesis: verum

end;

suppose A183: x0 = b ; :: thesis: diff (y1,x0) = diff (y2,x0)

then x0 in { r where r is Real : ( a <= r & r <= b ) } by A1;
then A184: x0 in [.a,b.] by RCOMP_1:def 1;
then A185: y1 is_differentiable_in x0 by A1, FDIFF_1:9;
then A186: ( y1 is_left_differentiable_in x0 & diff (y1,x0) = Ldiff (y1,x0) ) by FDIFF_3:22;
y2 is_differentiable_in x0 by A1, A184, FDIFF_1:9;
then A187: ( y2 is_left_differentiable_in x0 & diff (y2,x0) = Ldiff (y2,x0) ) by FDIFF_3:22;
then A188: y1 - y2 is_left_differentiable_in x0 by A186, FDIFF_3:11;
Ldiff (y1,x0) = Ldiff (y2,x0)

proof

A189: (Ldiff (y1,x0)) - (Ldiff (y2,x0)) = Ldiff ((y1 - y2),x0) by A186, A187, FDIFF_3:11;
for h being 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 A190: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Element of NAT holds h . n < 0 ) ) ; :: thesis: lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A191: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A192: 0 < b - a by A6, XREAL_1:50;
then consider n being Element of NAT such that
A193: for m being Element of NAT st n <= m holds
abs ((h . m) - 0) < (x0 - a) / 2 by A183, A191, SEQ_2:def 7;
A194: for p1 being real number st 0 < p1 holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0) < p1

proof

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

proof

let m be Element of NAT ; :: thesis: ( n <= m implies ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 )
assume A196: n <= m ; :: thesis: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
A197: abs ((h . m) - 0) < (x0 - a) / 2 by A193, A196;
A198: h . m < 0 by A190;
then A199: - (h . m) < (x0 - a) / 2 by A197, ABSVALUE:def 1;
A200: x0 + (h . m) <= b + 0 by A183, A198, XREAL_1:7;
x0 - ((x0 - a) / 2) <= x0 - (- (h . m)) by A199, XREAL_1:13;
then A201: (a + ((x0 - a) / 2)) - ((x0 - a) / 2) <= (x0 + (h . m)) - 0 by A183, A192, XREAL_1:13;
A202: [.a,b.] c= (dom y1) /\ (dom y2) by A1, XBOOLE_1:19;
then x0 in (dom y1) /\ (dom y2) by A184;
then A203: x0 in dom (y1 - y2) by VALUED_1:12;
A204: [.a,b.] c= dom (y1 - y2) by A202, VALUED_1:12;
x0 + (h . m) in { r where r is Real : ( a <= r & r <= b ) } by A200, A201;
then A205: x0 + (h . m) in [.a,b.] by RCOMP_1:def 1;
x0 in rng c1 by A190, TARSKI:def 1;
then A206: lim c1 = x0 by SEQ_4:25;
A207: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A206, SEQ_4:26 ;
A208: rng c1 c= dom (y1 - y2)

proof

for x being set st x in rng c1 holds
x in dom (y1 - y2) by A190, A203, TARSKI:def 1;
hence rng c1 c= dom (y1 - y2) by TARSKI:def 3; :: thesis: verum

end;

A209: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = ((h ") . m) * ((((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((y1 - y2) /* (h + c1)) . m) - (((y1 - y2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - (((y1 - y2) /* c1) . m)) by A190, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m))) by A208, FUNCT_2:108
.= ((h ") . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0)) by A206, A207, SEQ_4:26 ;
A210: (y1 - y2) . ((h . m) + x0) = (y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A204, A205, VALUED_1:13
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A205, FUNCT_1:49
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - ((y2 | [.a,b.]) . ((h . m) + x0)) by A205, FUNCT_1:49
.= 0 by A1 ;
(y1 - y2) . x0 = (y1 . x0) - (y2 . x0) by A203, VALUED_1:13
.= ((y1 | [.a,b.]) . x0) - (y2 . x0) by A184, FUNCT_1:49
.= ((y1 | [.a,b.]) . x0) - ((y2 | [.a,b.]) . x0) by A184, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A209, A210; :: thesis: verum

end;

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

end;

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

end;

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

end;

hence diff (y1,x0) = diff (y2,x0) by A185, A187, FDIFF_3:22; :: thesis: verum

end;

end;

end;

hence ((y1 `| Z) | AB) . x0 = ((y2 `| Z) | AB) . x0 by A127, A129, A130, A131, A132, FUNCT_1:49; :: thesis: verum

end;

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

end;

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

proof

A212: ( x1 `| Z is PartFunc of REAL,COMPLEX & y1 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A213: ( u01 is PartFunc of REAL,COMPLEX & v01 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( u01 (#) (x1 `| Z) is PartFunc of REAL,COMPLEX & v01 (#) (y1 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then A214: ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u01 (#) (x1 `| Z)) | AB) - ((v01 (#) (y1 `| Z)) | AB) by CFUNCT_1:55
.= ((u01 | AB) (#) ((x1 `| Z) | AB)) - ((v01 (#) (y1 `| Z)) | AB) by A212, A213, CFUNCT_1:53
.= ((u01 | AB) (#) ((x1 `| Z) | AB)) - ((v01 | AB) (#) ((y1 `| Z) | AB)) by A212, A213, CFUNCT_1:53 ;
A215: ( x2 `| Z is PartFunc of REAL,COMPLEX & y2 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A216: ( u02 is PartFunc of REAL,COMPLEX & v02 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( u02 (#) (x2 `| Z) is PartFunc of REAL,COMPLEX & v02 (#) (y2 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB = ((u02 (#) (x2 `| Z)) | AB) - ((v02 (#) (y2 `| Z)) | AB) by CFUNCT_1:55
.= ((u02 | AB) (#) ((x2 `| Z) | AB)) - ((v02 (#) (y2 `| Z)) | AB) by A215, A216, CFUNCT_1:53
.= ((u02 | AB) (#) ((x2 `| Z) | AB)) - ((v02 | AB) (#) ((y2 `| Z) | AB)) by A215, A216, CFUNCT_1:53 ;
hence ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB by A7, A24, A109, A126, A214; :: thesis: verum

end;

A217: integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b) = integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),AB) by INTEGRA5:19
.= integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),AB) by A211
.= integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) by INTEGRA5:19 ;
A218: ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB

proof

A219: ( x1 `| Z is PartFunc of REAL,COMPLEX & y1 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A220: ( v01 is PartFunc of REAL,COMPLEX & u01 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( v01 (#) (x1 `| Z) is PartFunc of REAL,COMPLEX & u01 (#) (y1 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then A221: ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v01 (#) (x1 `| Z)) | AB) + ((u01 (#) (y1 `| Z)) | AB) by CFUNCT_1:52
.= ((v01 | AB) (#) ((x1 `| Z) | AB)) + ((u01 (#) (y1 `| Z)) | AB) by A219, A220, CFUNCT_1:53
.= ((v01 | AB) (#) ((x1 `| Z) | AB)) + ((u01 | AB) (#) ((y1 `| Z) | AB)) by A219, A220, CFUNCT_1:53 ;
A222: ( x2 `| Z is PartFunc of REAL,COMPLEX & y2 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A223: ( v02 is PartFunc of REAL,COMPLEX & u02 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( v02 (#) (x2 `| Z) is PartFunc of REAL,COMPLEX & u02 (#) (y2 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB = ((v02 (#) (x2 `| Z)) | AB) + ((u02 (#) (y2 `| Z)) | AB) by CFUNCT_1:52
.= ((v02 | AB) (#) ((x2 `| Z) | AB)) + ((u02 (#) (y2 `| Z)) | AB) by A222, A223, CFUNCT_1:53
.= ((v02 | AB) (#) ((x2 `| Z) | AB)) + ((u02 | AB) (#) ((y2 `| Z) | AB)) by A222, A223, CFUNCT_1:53 ;
hence ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB by A7, A24, A109, A126, A221; :: thesis: verum

end;

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

end;

suppose A224: a = b ; :: thesis: integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z)

then reconsider BA = [.b,a.] as non empty closed_interval Subset of REAL by MEASURE5:14;
A225: integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b) = integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),BA) by A224, INTEGRA5:19;
A226: - (integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),BA)) = integral (((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))),a,b) by INTEGRA5:20;
A227: integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b) = integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),BA) by A224, INTEGRA5:19;
A228: - (integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),BA)) = integral (((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))),a,b) by INTEGRA5:20;
integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) = integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),BA) by A224, INTEGRA5:19;
then A229: integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b) = - (integral (((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))),a,b)) by INTEGRA5:20;
integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b) = integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),AB) by INTEGRA5:19;
then integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b) = - (integral (((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))),a,b)) by A224, INTEGRA5:20;
hence integral (f,x1,y1,a,b,Z) = integral (f,x2,y2,a,b,Z) by A2, A3, A225, A226, A227, A228, A229; :: thesis: verum

end;

end;