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

A4: now :: thesis: ( a = b or a < b )

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

end;

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 object st x0 in dom (u01 | AB) holds
x0 in dom (u02 | AB)

proof

let x0 be object ; :: 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 object st x0 in dom (u02 | AB) holds
x0 in dom (u01 | AB)

proof

let x0 be object ; :: 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:2; :: thesis: verum

end;

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

proof

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

end;

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

end;

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

proof

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

proof

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

A31: now :: thesis: ( x0 in ].a,b.[ or x0 = a or x0 = b )

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

A34: now :: thesis: ( a = x0 or a < x0 )

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

end;

A36: now :: thesis: ( x0 = b or x0 < b )

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

end;

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

end;

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

proof

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 non-zero 0 -convergent Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being Nat holds h . n > 0 ) holds
lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being 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 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 Nat holds h . n > 0 ) ) ; :: thesis: lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A46: ( h is convergent & lim h = 0 ) ;
A47: 0 < b - x0 by A6, A38, XREAL_1:50;
then consider n being Nat such that
A48: for m being Nat st n <= m holds
|.((h . m) - 0).| < (b - x0) / 2 by A46, SEQ_2:def 7;
A49: for p1 being Real st 0 < p1 holds
ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1

proof

let p1 be Real; :: thesis: ( 0 < p1 implies ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1 )
assume A50: 0 < p1 ; :: thesis: ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1
take n ; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1
for m being Nat st n <= m holds
((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0

proof

let m be 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: m in NAT by ORDINAL1:def 12;
A53: |.((h . m) - 0).| < (b - x0) / 2 by A48, A51;
A54: 0 < h . m by A45;
then A55: h . m < (b - x0) / 2 by A53, ABSVALUE:def 1;
A56: a + 0 <= x0 + (h . m) by A38, A54, XREAL_1:7;
x0 + (h . m) <= x0 + ((b - x0) / 2) by A55, XREAL_1:7;
then A57: (x0 + (h . m)) + 0 <= (b - ((b - x0) / 2)) + ((b - x0) / 2) by A47, XREAL_1:7;
A58: [.a,b.] c= (dom x1) /\ (dom x2) by A1, XBOOLE_1:19;
then x0 in (dom x1) /\ (dom x2) by A39;
then A59: x0 in dom (x1 - x2) by VALUED_1:12;
A60: [.a,b.] c= dom (x1 - x2) by A58, VALUED_1:12;
x0 + (h . m) in { r where r 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 A45, TARSKI:def 1;
A63: lim c1 = c1 . m by SEQ_4:26;
A64: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A62, A63, SEQ_4:25 ;
A65: rng c1 c= dom (x1 - x2) by A45, A59, TARSKI:def 1;
A66: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = ((h ") . m) * ((((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((x1 - x2) /* (h + c1)) . m) - (((x1 - x2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - (((x1 - x2) /* c1) . m)) by A45, FUNCT_2:108, A52
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m))) by A65, FUNCT_2:108, A52
.= ((h ") . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0)) by A62, A63, A64, SEQ_4:25 ;
A67: (x1 - x2) . ((h . m) + x0) = (x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A60, A61, VALUED_1:13
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A61, FUNCT_1:49
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - ((x2 | [.a,b.]) . ((h . m) + x0)) by A61, FUNCT_1:49
.= 0 by A1 ;
(x1 - x2) . x0 = (x1 . x0) - (x2 . x0) by A59, VALUED_1:13
.= ((x1 | [.a,b.]) . x0) - (x2 . x0) by A39, FUNCT_1:49
.= ((x1 | [.a,b.]) . x0) - ((x2 | [.a,b.]) . x0) by A39, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A66, A67; :: thesis: verum

end;

hence for m being Nat st n <= m holds
|.((((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 A68: x0 in ].a,b.[ ; :: thesis: diff (x1,x0) = diff (x2,x0)

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

proof

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

proof

let x0 be object ; :: 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 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.] ; :: thesis: verum

end;

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

proof

let x0 be object ; :: 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:61
.= ].a,b.[ by A1, A70, XBOOLE_1:1, XBOOLE_1:28 ;
then (x1 | ].a,b.[) . x0 = x1 . x0 by A80, FUNCT_1:49
.= (x1 | [.a,b.]) . x0 by A70, A80, A81, FUNCT_1:49
.= x2 . x0 by A70, A80, A81, A1, FUNCT_1:49
.= (x2 | ].a,b.[) . x0 by A80, A81, FUNCT_1:49 ;
hence (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:2; :: 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:9;
then A85: ( x1 is_left_differentiable_in x0 & diff (x1,x0) = Ldiff (x1,x0) ) by FDIFF_3:22;
x2 is_differentiable_in x0 by A1, A83, FDIFF_1:9;
then A86: ( x2 is_left_differentiable_in x0 & diff (x2,x0) = Ldiff (x2,x0) ) by FDIFF_3:22;
then A87: x1 - x2 is_left_differentiable_in x0 by A85, FDIFF_3:11;
Ldiff (x1,x0) = Ldiff (x2,x0)

proof

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

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (x1 - x2) & ( for n being 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 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 Nat holds h . n < 0 ) ) ; :: thesis: lim ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) = 0
A90: ( h is convergent & lim h = 0 ) ;
A91: 0 < b - a by A6, XREAL_1:50;
then consider n being Nat such that
A92: for m being Nat st n <= m holds
|.((h . m) - 0).| < (x0 - a) / 2 by A82, A90, SEQ_2:def 7;
A93: for p1 being Real st 0 < p1 holds
ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1

proof

let p1 be Real; :: thesis: ( 0 < p1 implies ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1 )
assume A94: 0 < p1 ; :: thesis: ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1
take n ; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1
for m being Nat st n <= m holds
((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0

proof

let m be 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: m in NAT by ORDINAL1:def 12;
A97: |.((h . m) - 0).| < (x0 - a) / 2 by A92, A95;
A98: h . m < 0 by A89;
then A99: - (h . m) < (x0 - a) / 2 by A97, ABSVALUE:def 1;
A100: x0 + (h . m) <= b + 0 by A82, A98, XREAL_1:7;
x0 - ((x0 - a) / 2) <= x0 - (- (h . m)) by A99, XREAL_1:13;
then A101: (a + ((x0 - a) / 2)) - ((x0 - a) / 2) <= (x0 + (h . m)) - 0 by A82, A91, XREAL_1:13;
A102: [.a,b.] c= (dom x1) /\ (dom x2) by A1, XBOOLE_1:19;
then x0 in (dom x1) /\ (dom x2) by A83;
then A103: x0 in dom (x1 - x2) by VALUED_1:12;
A104: [.a,b.] c= dom (x1 - x2) by A102, VALUED_1:12;
x0 + (h . m) in { r where r is Real : ( a <= r & r <= b ) } by A100, A101;
then A105: x0 + (h . m) in [.a,b.] by RCOMP_1:def 1;
x0 in rng c1 by A89, TARSKI:def 1;
then A106: lim c1 = x0 by SEQ_4:25;
A107: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A106, SEQ_4:26 ;
A108: rng c1 c= dom (x1 - x2) by A89, A103, TARSKI:def 1;
A109: ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = ((h ") . m) * ((((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((x1 - x2) /* (h + c1)) . m) - (((x1 - x2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - (((x1 - x2) /* c1) . m)) by A89, FUNCT_2:108, A96
.= ((h ") . m) * (((x1 - x2) . ((h + c1) . m)) - ((x1 - x2) . (c1 . m))) by A108, FUNCT_2:108, A96
.= ((h ") . m) * (((x1 - x2) . ((h . m) + x0)) - ((x1 - x2) . x0)) by A106, A107, SEQ_4:26 ;
A110: (x1 - x2) . ((h . m) + x0) = (x1 . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A104, A105, VALUED_1:13
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - (x2 . ((h . m) + x0)) by A105, FUNCT_1:49
.= ((x1 | [.a,b.]) . ((h . m) + x0)) - ((x2 | [.a,b.]) . ((h . m) + x0)) by A105, FUNCT_1:49
.= 0 by A1 ;
(x1 - x2) . x0 = (x1 . x0) - (x2 . x0) by A103, VALUED_1:13
.= ((x1 | [.a,b.]) . x0) - (x2 . x0) by A83, FUNCT_1:49
.= ((x1 | [.a,b.]) . x0) - ((x2 | [.a,b.]) . x0) by A83, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m = 0 by A109, A110; :: thesis: verum

end;

hence for m being Nat st n <= m holds
|.((((h ") (#) (((x1 - x2) /* (h + c1)) - ((x1 - x2) /* c1))) . m) - 0).| < p1 by A94, 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 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 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;

A111: v01 | AB = v02 | AB

proof

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

proof

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

proof

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

end;

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

proof

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

proof

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

A135: now :: thesis: ( x0 in ].a,b.[ or x0 = a or x0 = b )

assume A136: ( 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 A129, A131, RCOMP_1:def 1;
then A137: ex r being Real st
( r = x0 & a <= r & r <= b ) ;

A138: now :: thesis: ( a = x0 or a < x0 )

assume A139: ( 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 A137, A139; :: thesis: verum

end;

A140: now :: thesis: ( x0 = b or x0 < b )

assume A141: ( 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 A137, A141; :: thesis: verum

end;

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

end;

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

proof

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

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:9;
then A145: ( y1 is_right_differentiable_in x0 & diff (y1,x0) = Rdiff (y1,x0) ) by FDIFF_3:22;
y2 is_differentiable_in x0 by A1, A143, FDIFF_1:9;
then A146: ( y2 is_right_differentiable_in x0 & diff (y2,x0) = Rdiff (y2,x0) ) by FDIFF_3:22;
then A147: y1 - y2 is_right_differentiable_in x0 by A145, FDIFF_3:17;
Rdiff (y1,x0) = Rdiff (y2,x0)

proof

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

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being 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 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 Nat holds h . n > 0 ) ) ; :: thesis: lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A150: ( h is convergent & lim h = 0 ) ;
A151: 0 < b - x0 by A6, A142, XREAL_1:50;
then consider n being Nat such that
A152: for m being Nat st n <= m holds
|.((h . m) - 0).| < (b - x0) / 2 by A150, SEQ_2:def 7;
A153: for p1 being Real st 0 < p1 holds
ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1

proof

let p1 be Real; :: thesis: ( 0 < p1 implies ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1 )
assume A154: 0 < p1 ; :: thesis: ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1
take n ; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1
for m being Nat st n <= m holds
((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0

proof

let m be 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: |.((h . m) - 0).| < (b - x0) / 2 by A152, A155;
A157: m in NAT by ORDINAL1:def 12;
A158: 0 < h . m by A149;
then A159: h . m < (b - x0) / 2 by A156, ABSVALUE:def 1;
A160: a + 0 <= x0 + (h . m) by A142, A158, XREAL_1:7;
x0 + (h . m) <= x0 + ((b - x0) / 2) by A159, XREAL_1:7;
then A161: (x0 + (h . m)) + 0 <= (b - ((b - x0) / 2)) + ((b - x0) / 2) by A151, XREAL_1:7;
A162: [.a,b.] c= (dom y1) /\ (dom y2) by A1, XBOOLE_1:19;
then x0 in (dom y1) /\ (dom y2) by A143;
then A163: x0 in dom (y1 - y2) by VALUED_1:12;
A164: [.a,b.] c= dom (y1 - y2) by A162, VALUED_1:12;
x0 + (h . m) in { r where r is Real : ( a <= r & r <= b ) } by A160, A161;
then A165: x0 + (h . m) in [.a,b.] by RCOMP_1:def 1;
A166: x0 in rng c1 by A149, TARSKI:def 1;
A167: lim c1 = c1 . m by SEQ_4:26;
A168: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A167, A166, SEQ_4:25 ;
A169: rng c1 c= dom (y1 - y2) by A163, A149, TARSKI:def 1;
A170: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = ((h ") . m) * ((((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((y1 - y2) /* (h + c1)) . m) - (((y1 - y2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - (((y1 - y2) /* c1) . m)) by A149, FUNCT_2:108, A157
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m))) by A169, FUNCT_2:108, A157
.= ((h ") . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0)) by A166, A167, A168, SEQ_4:25 ;
A171: (y1 - y2) . ((h . m) + x0) = (y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A164, A165, VALUED_1:13
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A165, FUNCT_1:49
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - ((y2 | [.a,b.]) . ((h . m) + x0)) by A165, FUNCT_1:49
.= 0 by A1 ;
(y1 - y2) . x0 = (y1 . x0) - (y2 . x0) by A163, VALUED_1:13
.= ((y1 | [.a,b.]) . x0) - (y2 . x0) by A143, FUNCT_1:49
.= ((y1 | [.a,b.]) . x0) - ((y2 | [.a,b.]) . x0) by A143, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A170, A171; :: thesis: verum

end;

hence for m being Nat st n <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1 by A154, 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 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 A172: x0 in ].a,b.[ ; :: thesis: diff (y1,x0) = diff (y2,x0)

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

proof

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

proof

let x0 be object ; :: thesis: ( x0 in ].a,b.[ implies x0 in [.a,b.] )
assume A175: x0 in ].a,b.[ ; :: thesis: x0 in [.a,b.]
x0 in { r where r is Real : ( a < r & r < b ) } by A175, RCOMP_1:def 2;
then A176: ex r being 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 A176;
hence x0 in [.a,b.] by RCOMP_1:def 1; :: thesis: verum

end;

hence ].a,b.[ c= [.a,b.] ; :: thesis: verum

end;

then A177: y1 is_differentiable_on ].a,b.[ by A1, A173, FDIFF_1:26, XBOOLE_1:1;
then A178: ( y1 | ].a,b.[ is_differentiable_on ].a,b.[ & (y1 | ].a,b.[) `| ].a,b.[ = y1 `| ].a,b.[ ) by FDIFF_2:16;
A179: (y1 `| ].a,b.[) . x0 = diff (y1,x0) by A172, A177, FDIFF_1:def 7;
A180: y2 is_differentiable_on ].a,b.[ by A1, A173, A174, FDIFF_1:26, XBOOLE_1:1;
then A181: ( y2 | ].a,b.[ is_differentiable_on ].a,b.[ & (y2 | ].a,b.[) `| ].a,b.[ = y2 `| ].a,b.[ ) by FDIFF_2:16;
A182: (y2 `| ].a,b.[) . x0 = diff (y2,x0) by A172, A180, FDIFF_1:def 7;
A183: dom (y1 | ].a,b.[) = (dom y1) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A1, A174, XBOOLE_1:1, XBOOLE_1:28
.= (dom y2) /\ ].a,b.[ by A1, A174, XBOOLE_1:1, XBOOLE_1:28
.= dom (y2 | ].a,b.[) by RELAT_1:61 ;
for x0 being object st x0 in dom (y1 | ].a,b.[) holds
(y1 | ].a,b.[) . x0 = (y2 | ].a,b.[) . x0

proof

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

end;

hence diff (y1,x0) = diff (y2,x0) by A178, A179, A181, A182, A183, FUNCT_1:2; :: thesis: verum

end;

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

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

proof

A192: (Ldiff (y1,x0)) - (Ldiff (y2,x0)) = Ldiff ((y1 - y2),x0) by A189, A190, FDIFF_3:11;
for h being non-zero 0 -convergent Real_Sequence
for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Nat holds h . n < 0 ) holds
lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c1 being constant Real_Sequence st rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being 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 Nat holds h . n < 0 ) implies lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0 )
assume A193: ( rng c1 = {x0} & rng (h + c1) c= dom (y1 - y2) & ( for n being Nat holds h . n < 0 ) ) ; :: thesis: lim ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) = 0
A194: ( h is convergent & lim h = 0 ) ;
A195: 0 < b - a by A6, XREAL_1:50;
then consider n being Nat such that
A196: for m being Nat st n <= m holds
|.((h . m) - 0).| < (x0 - a) / 2 by A186, A194, SEQ_2:def 7;
A197: for p1 being Real st 0 < p1 holds
ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1

proof

let p1 be Real; :: thesis: ( 0 < p1 implies ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1 )
assume A198: 0 < p1 ; :: thesis: ex n1 being Nat st
for m being Nat st n1 <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1
take n ; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1
for m being Nat st n <= m holds
((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0

proof

let m be Nat; :: thesis: ( n <= m implies ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 )
assume A199: n <= m ; :: thesis: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0
A200: |.((h . m) - 0).| < (x0 - a) / 2 by A196, A199;
A201: m in NAT by ORDINAL1:def 12;
A202: h . m < 0 by A193;
then A203: - (h . m) < (x0 - a) / 2 by A200, ABSVALUE:def 1;
A204: x0 + (h . m) <= b + 0 by A186, A202, XREAL_1:7;
x0 - ((x0 - a) / 2) <= x0 - (- (h . m)) by A203, XREAL_1:13;
then A205: (a + ((x0 - a) / 2)) - ((x0 - a) / 2) <= (x0 + (h . m)) - 0 by A186, A195, XREAL_1:13;
A206: [.a,b.] c= (dom y1) /\ (dom y2) by A1, XBOOLE_1:19;
then x0 in (dom y1) /\ (dom y2) by A187;
then A207: x0 in dom (y1 - y2) by VALUED_1:12;
A208: [.a,b.] c= dom (y1 - y2) by A206, VALUED_1:12;
x0 + (h . m) in { r where r is Real : ( a <= r & r <= b ) } by A204, A205;
then A209: x0 + (h . m) in [.a,b.] by RCOMP_1:def 1;
x0 in rng c1 by A193, TARSKI:def 1;
then A210: lim c1 = x0 by SEQ_4:25;
A211: (h + c1) . m = (h . m) + (c1 . m) by SEQ_1:7
.= (h . m) + x0 by A210, SEQ_4:26 ;
A212: rng c1 c= dom (y1 - y2) by A193, A207, TARSKI:def 1;
A213: ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = ((h ") . m) * ((((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1)) . m) by SEQ_1:8
.= ((h ") . m) * ((((y1 - y2) /* (h + c1)) . m) - (((y1 - y2) /* c1) . m)) by RFUNCT_2:1
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - (((y1 - y2) /* c1) . m)) by A193, FUNCT_2:108, A201
.= ((h ") . m) * (((y1 - y2) . ((h + c1) . m)) - ((y1 - y2) . (c1 . m))) by A212, FUNCT_2:108, A201
.= ((h ") . m) * (((y1 - y2) . ((h . m) + x0)) - ((y1 - y2) . x0)) by A210, A211, SEQ_4:26 ;
A214: (y1 - y2) . ((h . m) + x0) = (y1 . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A208, A209, VALUED_1:13
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - (y2 . ((h . m) + x0)) by A209, FUNCT_1:49
.= ((y1 | [.a,b.]) . ((h . m) + x0)) - ((y2 | [.a,b.]) . ((h . m) + x0)) by A209, FUNCT_1:49
.= 0 by A1 ;
(y1 - y2) . x0 = (y1 . x0) - (y2 . x0) by A207, VALUED_1:13
.= ((y1 | [.a,b.]) . x0) - (y2 . x0) by A187, FUNCT_1:49
.= ((y1 | [.a,b.]) . x0) - ((y2 | [.a,b.]) . x0) by A187, FUNCT_1:49
.= 0 by A1 ;
hence ((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m = 0 by A213, A214; :: thesis: verum

end;

hence for m being Nat st n <= m holds
|.((((h ") (#) (((y1 - y2) /* (h + c1)) - ((y1 - y2) /* c1))) . m) - 0).| < p1 by A198, 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 A197, SEQ_2:def 7; :: thesis: verum

end;

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

end;

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

end;

end;

end;

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

end;

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

end;

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

proof

A216: ( x1 `| Z is PartFunc of REAL,COMPLEX & y1 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A217: ( u01 is PartFunc of REAL,COMPLEX & v01 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( u01 (#) (x1 `| Z) is PartFunc of REAL,COMPLEX & v01 (#) (y1 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then A218: ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u01 (#) (x1 `| Z)) | AB) - ((v01 (#) (y1 `| Z)) | AB) by CFUNCT_1:55
.= ((u01 | AB) (#) ((x1 `| Z) | AB)) - ((v01 (#) (y1 `| Z)) | AB) by A216, A217, CFUNCT_1:53
.= ((u01 | AB) (#) ((x1 `| Z) | AB)) - ((v01 | AB) (#) ((y1 `| Z) | AB)) by A216, A217, CFUNCT_1:53 ;
A219: ( x2 `| Z is PartFunc of REAL,COMPLEX & y2 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A220: ( u02 is PartFunc of REAL,COMPLEX & v02 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( u02 (#) (x2 `| Z) is PartFunc of REAL,COMPLEX & v02 (#) (y2 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB = ((u02 (#) (x2 `| Z)) | AB) - ((v02 (#) (y2 `| Z)) | AB) by CFUNCT_1:55
.= ((u02 | AB) (#) ((x2 `| Z) | AB)) - ((v02 (#) (y2 `| Z)) | AB) by A219, A220, CFUNCT_1:53
.= ((u02 | AB) (#) ((x2 `| Z) | AB)) - ((v02 | AB) (#) ((y2 `| Z) | AB)) by A219, A220, CFUNCT_1:53 ;
hence ((u01 (#) (x1 `| Z)) - (v01 (#) (y1 `| Z))) | AB = ((u02 (#) (x2 `| Z)) - (v02 (#) (y2 `| Z))) | AB by A7, A24, A111, A128, A218; :: thesis: verum

end;

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

proof

A223: ( x1 `| Z is PartFunc of REAL,COMPLEX & y1 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A224: ( v01 is PartFunc of REAL,COMPLEX & u01 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( v01 (#) (x1 `| Z) is PartFunc of REAL,COMPLEX & u01 (#) (y1 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then A225: ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v01 (#) (x1 `| Z)) | AB) + ((u01 (#) (y1 `| Z)) | AB) by CFUNCT_1:52
.= ((v01 | AB) (#) ((x1 `| Z) | AB)) + ((u01 (#) (y1 `| Z)) | AB) by A223, A224, CFUNCT_1:53
.= ((v01 | AB) (#) ((x1 `| Z) | AB)) + ((u01 | AB) (#) ((y1 `| Z) | AB)) by A223, A224, CFUNCT_1:53 ;
A226: ( x2 `| Z is PartFunc of REAL,COMPLEX & y2 `| Z is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
A227: ( v02 is PartFunc of REAL,COMPLEX & u02 is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
( v02 (#) (x2 `| Z) is PartFunc of REAL,COMPLEX & u02 (#) (y2 `| Z) is PartFunc of REAL,COMPLEX ) by NUMBERS:11, RELSET_1:7;
then ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB = ((v02 (#) (x2 `| Z)) | AB) + ((u02 (#) (y2 `| Z)) | AB) by CFUNCT_1:52
.= ((v02 | AB) (#) ((x2 `| Z) | AB)) + ((u02 (#) (y2 `| Z)) | AB) by A226, A227, CFUNCT_1:53
.= ((v02 | AB) (#) ((x2 `| Z) | AB)) + ((u02 | AB) (#) ((y2 `| Z) | AB)) by A226, A227, CFUNCT_1:53 ;
hence ((v01 (#) (x1 `| Z)) + (u01 (#) (y1 `| Z))) | AB = ((v02 (#) (x2 `| Z)) + (u02 (#) (y2 `| Z))) | AB by A7, A24, A111, A128, A225; :: 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 A222
.= 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, A221; :: thesis: verum

end;

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

end;

end;