:: Complex Integral
:: by Masahiko Yamazaki , Hiroshi Yamazaki , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 10, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FDIFF_1, SEQ_1, FUNCT_1, ZFMISC_1, MCART_1,
ARYTM_3, RELAT_1, XCMPLX_0, REAL_1, PARTFUN1, INTEGRA1, COMPLEX1,
VALUED_1, ARYTM_1, XBOOLE_0, TARSKI, XXREAL_0, XXREAL_1, RCOMP_1,
ORDINAL2, SIN_COS, CARD_1, FDIFF_3, FUNCT_2, SEQ_2, TOPMETR, INTEGRA5,
VFUNCT_1, XXREAL_2, INTEGR1C, MEASURE5, VALUED_0, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
RELSET_1, VALUED_0, FUNCT_3, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, REAL_1, BINOP_1, RCOMP_1, SEQ_1,
SEQ_2, FCONT_1, FDIFF_1, COMSEQ_3, TOPMETR, MCART_1, MEASURE5, INTEGRA5,
SIN_COS, VALUED_1, PRE_TOPC, FDIFF_3, STRUCT_0, XXREAL_2;
constructors REAL_1, FDIFF_1, RFUNCT_3, FCONT_1, INTEGRA5, SIN_COS, TOPMETR,
FDIFF_3, MESFUN6C, SEQ_2, RVSUM_1, COMSEQ_3, INTEGRA1, COMSEQ_2,
XTUPLE_0, BINOP_2, BINOP_1;
registrations XREAL_0, FUNCT_2, NUMBERS, ORDINAL1, MEMBERED, SIN_COS, FDIFF_1,
SUBSET_1, XCMPLX_0, RELAT_1, XXREAL_0, XBOOLE_0, VALUED_0, VALUED_1,
RELSET_1, MEASURE5, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI;
equalities INTEGRA5, VALUED_1;
expansions TARSKI;
theorems ZFMISC_1, XCMPLX_0, TOPMETR, SEQ_4, INTEGRA1, RFUNCT_1, FUNCT_1,
SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, COMPLEX1, FUNCT_3, TARSKI, RCOMP_1,
FCONT_1, RFUNCT_2, FDIFF_2, RELAT_1, XXREAL_1, FUNCT_2, NUMBERS,
XBOOLE_0, XBOOLE_1, XREAL_1, INTEGRA5, SIN_COS, INTEGRA6, CFUNCT_1,
VALUED_1, MESFUN6C, TOPS_1, FDIFF_3, RELSET_1, XXREAL_2, MCART_1,
BORSUK_5, COMSEQ_3, MEASURE5, XREAL_0, ORDINAL1;
schemes FUNCT_2, FUNCT_7;
begin :: The Definition of Complex Curve and Complex Integral
reserve n,n1,m for Element of NAT;
reserve r,t,x1 for Real;
reserve h for 0-convergent non-zero Real_Sequence;
reserve c1 for constant Real_Sequence;
reserve p1 for Real;
definition
func R2-to-C -> Function of [:REAL,REAL:],COMPLEX means :Def1:
for p be Element of [:REAL,REAL:], a,b be Element of REAL st
a = p`1 & b = p`2 holds
it.([a,b]) = a+b*<i>;
existence
proof
deffunc F(Real,Real)
= $1+$2*<i>;
A1: for x being Element of REAL, y being Element of REAL holds
F(x,y) in COMPLEX by XCMPLX_0:def 2;
consider
f being Function of [:REAL,REAL:],COMPLEX such that
A2: for x,y being Element of REAL
holds f.(x,y) = F(x,y) from FUNCT_7:sch 1(A1);
deffunc G(Element of [:REAL,REAL:]) = f.($1`1,$1`2);
A3: now let p being Element of [:REAL,REAL:];
p`1 is Element of REAL & p`2 is Element of REAL by MCART_1:10;then
consider a,b be Element of REAL such that
A4: a = p`1 & b = p`2;
G(p) = a + b*<i> by A2,A4;
hence G(p) in COMPLEX by XCMPLX_0:def 2;
end;
consider g being Function of [:REAL,REAL:], COMPLEX such that
A5: for p being Element of [:REAL,REAL:]
holds g.p = G(p) from FUNCT_2:sch 8(A3);
take g;
for p be Element of [:REAL,REAL:], a,b be Element of REAL st
a = p`1 & b = p`2 holds
g.([a,b]) =a+b*<i>
proof
let p be Element of [:REAL,REAL:],
a,b be Element of REAL such that
A6: a = p`1 & b = p`2;
A8: [a,b] is Element of [:REAL,REAL:] by ZFMISC_1:def 2;
A9: [a,b]`1 = p`1 by A6;
[a,b]`2 = p`2 by A6;then
g.([a,b]) = f.(a,b) by A5,A8,A9
.= a+b*<i> by A2;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f,g be Function of [:REAL,REAL:],COMPLEX;
assume
A10: for p be Element of [:REAL,REAL:],
a,b be Element of REAL st a = p`1 & b = p`2
holds f.([a,b]) = a+b*<i>;
assume
A11: for p be Element of [:REAL,REAL:],
a,b be Element of REAL st a = p`1 & b = p`2
holds g.([a,b]) = a+b*<i>;
for p0 be object st p0 in [:REAL,REAL:] holds f.p0 = g.p0
proof
let p0 be object;
assume
A12: p0 in [:REAL,REAL:];then
consider x0,y0 be object such that
A13: x0 in REAL & y0 in REAL & p0 = [x0,y0] by ZFMISC_1:def 2;
reconsider a = x0,b = y0 as Element of REAL by A13;
A14: p0`1 = a by A13;
A15: p0`2 = b by A13;
then f.p0 = a+b*<i> by A12,A10,A14,A13
.= g.p0 by A13,A12,A11,A14,A15;
hence thesis;
end;
hence f = g by FUNCT_2:12;
end;
end;
definition
let a,b be Real;
let x,y be PartFunc of REAL,REAL, Z be Subset of REAL;
let f be PartFunc of COMPLEX, COMPLEX;
func integral(f,x,y,a,b,Z) -> Complex means :Def2:
ex u0, v0 be PartFunc of REAL,REAL st
u0 = (Re f)* (R2-to-C) *<:x,y:> & v0 = (Im f)* (R2-to-C) *<:x,y:> &
it = integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i>;
existence
proof
A1: dom <:x,y:> = dom x /\ dom y by FUNCT_3:def 7;
rng <:x,y:> c= [:rng x,rng y:] by FUNCT_3:51;then
rng <:x,y:> c= [:REAL,REAL:] by XBOOLE_1:1;then
reconsider xy=<:x,y:> as PartFunc of REAL,[:REAL,REAL:]
by A1,RELSET_1:4;
(Re f)* (R2-to-C) *xy is PartFunc of REAL,REAL;then
reconsider u0=(Re f)* (R2-to-C) *<:x,y:> as PartFunc of REAL,REAL;
(Im f)* (R2-to-C) *xy is PartFunc of REAL,REAL;
then
reconsider v0=(Im f)* (R2-to-C) *<:x,y:> as PartFunc of REAL,REAL;
integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i>
is Complex;
hence thesis;
end;
uniqueness;
end;
definition
let C be PartFunc of REAL,COMPLEX;
attr C is C1-curve-like means :Def3:
ex a,b be Real,
x,y be PartFunc of REAL,REAL, Z be Subset of REAL st
a <= b & [.a,b.]=dom C & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z is open & [.a,b.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous & y`|Z is continuous &
C = (x+<i>(#)y) | [.a,b.];
end;
registration
cluster C1-curve-like for PartFunc of REAL,COMPLEX;
existence
proof
set a = 1, b = 2;
set x = cos, y = sin;
set Z = ].-5,5.[; ::!!!!
consider C be PartFunc of REAL,COMPLEX such that
A1: C = (x+<i>(#)y) | [.a,b.];
take C;
A2: dom (x+<i>(#)y) = REAL by FUNCT_2:def 1;
dom C = dom (x+<i>(#)y) /\ [.a,b.] by A1,RELAT_1:61;then
A3: [.a,b.] = dom C by A2,XBOOLE_1:28;
A4: Z is open by RCOMP_1:7;
A5: [.a,b.] c= Z by XXREAL_1:47;
A6: x is_differentiable_on Z by A4,FDIFF_1:26,SIN_COS:67;
A7: y is_differentiable_on Z by A4,FDIFF_1:26,SIN_COS:68;
sin = sin|(REAL);
then sin|Z is continuous by FCONT_1:16;then
(-sin)|Z is continuous by FCONT_1:21,SIN_COS:24;then
A8: -sin|Z is continuous by RFUNCT_1:46;
A9: dom(-sin|Z) = dom((-sin)|Z) by RFUNCT_1:46
.= dom(-sin) /\ Z by RELAT_1:61
.= REAL /\ Z by SIN_COS:24,VALUED_1:8
.= Z by XBOOLE_1:28;
for x1 st x1 in Z holds (-sin|Z).x1 = diff(x,x1)
proof
let x1 such that
A10: x1 in Z;
reconsider x1 as Element of REAL by XREAL_0:def 1;
A11: (-sin|Z).x1 = ((-sin)|Z).x1 by RFUNCT_1:46
.= (-sin).x1 by A10,FUNCT_1:49
.= -(sin.x1) by RFUNCT_1:58
.= -sin|Z.x1 by A10,FUNCT_1:49;
diff(x,x1) = -sin.x1 by SIN_COS:67
.= (-sin|Z).x1 by A11,A10,FUNCT_1:49;
hence thesis;
end; then
A12: x`|Z is continuous by A6,A8,A9,FDIFF_1:def 7;
cos = cos|(REAL);
then A13: cos|Z is continuous by FCONT_1:16;
A14: dom(cos|Z) = dom(cos) /\ Z by RELAT_1:61
.= Z by SIN_COS:24,XBOOLE_1:28;
for x1 st x1 in Z holds (cos|Z).x1 = diff(y,x1)
proof
let x1 such that
A15: x1 in Z;
diff(y,x1) = cos.x1 by SIN_COS:68
.= (cos|Z).x1 by A15,FUNCT_1:49;
hence thesis;
end;
then y`|Z is continuous by A7,A13,A14,FDIFF_1:def 7;
hence thesis by A1,A3,A4,A5,A6,A7,A12,SIN_COS:24;
end;
end;
definition
mode C1-curve is C1-curve-like PartFunc of REAL,COMPLEX;
end;
Lm1: for a,b be Real, x,y be PartFunc of REAL,REAL, Z1,Z2 be Subset of REAL,
f be PartFunc of COMPLEX, COMPLEX st
a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 &
x is_differentiable_on Z2 & y is_differentiable_on Z2 &
rng ( (x + <i>(#)y) | [.a,b.] ) c= dom f
holds
integral(f,x,y,a,b,Z1) = integral(f,x,y,a,b,Z2)
proof
let a,b be Real,
x,y be PartFunc of REAL,REAL,
Z1,Z2 be Subset of REAL,
f be PartFunc of COMPLEX, COMPLEX;
assume
A1: a <= b & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z1 is open & Z2 is open & [.a,b.] c= Z1 & Z1 c= Z2 &
x is_differentiable_on Z2 & y is_differentiable_on Z2 &
rng ( (x + <i>(#)y) | [.a,b.] ) c=dom f;
then
A2: x is_differentiable_on Z1 & y is_differentiable_on Z1 by FDIFF_1:26;
consider u01,v01 be PartFunc of REAL,REAL such that
A3: u01=(Re f)* (R2-to-C) *<:x,y:> & v01=(Im f)* (R2-to-C) *<:x,y:> &
integral(f,x,y,a,b,Z1)= integral( u01(#)(x`|Z1) - v01(#)(y`|Z1) ,a,b )
+ integral( v01(#)(x`|Z1) + u01(#)(y`|Z1),a,b )*<i> by Def2;
consider u02,v02 be PartFunc of REAL,REAL such that
A4: u02=(Re f)* (R2-to-C) *<:x,y:> & v02=(Im f)* (R2-to-C) *<:x,y:> &
integral(f,x,y,a,b,Z2)= integral( u02(#)(x`|Z2) - v02(#)(y`|Z2) ,a,b )
+ integral( v02(#)(x`|Z2) + u02(#)(y`|Z2) ,a,b )*<i> by Def2;
reconsider AB=[.a,b.] as non empty closed_interval Subset of REAL
by A1,MEASURE5:14;
A5: (u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB = (u02(#)(x`|Z2) - v02(#)(y`|Z2)) | AB
proof
dom(u01(#)(x`|Z1) - v01(#)(y`|Z1))
= dom(u01(#)(x`|Z1)) /\ dom(v01(#)(y`|Z1)) by VALUED_1:12
.= (dom u01 /\ dom(x`|Z1)) /\ dom(v01(#)(y`|Z1)) by VALUED_1:def 4
.= (dom u01 /\ dom(x`|Z1)) /\ (dom v01 /\ dom (y`|Z1))
by VALUED_1:def 4;then
A6: dom(u01(#)(x`|Z1) - v01(#)(y`|Z1))
= (dom u01 /\ Z1) /\ ( dom v01 /\ dom(y`|Z1)) by A2,FDIFF_1:def 7
.= (dom u01 /\ Z1) /\ ( dom v01 /\ Z1) by A2,FDIFF_1:def 7
.= dom u01 /\ (Z1 /\ ( dom v01 /\ Z1)) by XBOOLE_1:16
.= dom u01 /\ ((Z1 /\ Z1 ) /\ dom v01) by XBOOLE_1:16
.= (dom u01 /\ dom v01) /\ Z1 by XBOOLE_1:16;
dom(u02(#)(x`|Z2) - v02(#)(y`|Z2))
= dom(u02(#)(x`|Z2)) /\ dom(v02(#)(y`|Z2)) by VALUED_1:12
.= (dom u02 /\ dom(x`|Z2)) /\ dom(v02(#)(y`|Z2)) by VALUED_1:def 4
.= (dom u02 /\ dom(x`|Z2)) /\ (dom v02 /\ dom (y`|Z2))
by VALUED_1:def 4;then
A7: dom(u02(#)(x`|Z2) - v02(#)(y`|Z2))
= (dom u02 /\ Z2) /\ ( dom v02 /\ dom(y`|Z2)) by A1,FDIFF_1:def 7
.= (dom u02 /\ Z2) /\ ( dom v02 /\ Z2) by A1,FDIFF_1:def 7
.= dom u02 /\ (Z2 /\ ( dom v02 /\ Z2)) by XBOOLE_1:16
.= dom u02 /\ ((Z2 /\ Z2 ) /\ dom v02) by XBOOLE_1:16
.= (dom u01 /\ dom v01) /\ Z2 by A3,A4,XBOOLE_1:16;
A8: dom((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB)
= dom (u01(#)(x`|Z1) - v01(#)(y`|Z1)) /\ AB by RELAT_1:61
.= (dom u01 /\ dom v01) /\ (Z1 /\ AB) by A6,XBOOLE_1:16
.= (dom u01 /\ dom v01) /\ AB by A1,XBOOLE_1:28;
A9: dom((u02(#)(x`|Z2) - v02(#)(y`|Z2)) | AB)
= dom (u02(#)(x`|Z2) - v02(#)(y`|Z2)) /\ AB by RELAT_1:61
.= (dom u01 /\ dom v01) /\ (Z2 /\ AB) by A7,XBOOLE_1:16
.= (dom u01 /\ dom v01) /\ AB by A1,XBOOLE_1:1,28;
for x0 being object st x0 in dom((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB )
holds
((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB).x0
= ((u02(#)(x`|Z2) - v02(#)(y`|Z2)) | AB ).x0
proof
let x0 being object such that
A10: x0 in dom((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB );
x0 in dom(u01(#)(x`|Z1) - v01(#)(y`|Z1)) /\ AB by A10,RELAT_1:61;
then
A11: x0 in dom(u01(#)(x`|Z1) - v01(#)(y`|Z1)) by XBOOLE_0:def 4;
then
x0 in dom(u01(#)(x`|Z1)) /\ dom(v01(#)(y`|Z1)) by VALUED_1:12;
then
A12: x0 in dom(u01(#)(x`|Z1)) & x0 in dom(v01(#)(y`|Z1))
by XBOOLE_0:def 4;then
x0 in dom u01 /\ dom(x`|Z1) & x0 in dom v01 /\ dom(y`|Z1)
by VALUED_1:def 4; then
x0 in dom u01 & x0 in dom(x`|Z1)
& x0 in dom v01 & x0 in dom(y`|Z1) by XBOOLE_0:def 4; then
A13: x0 in Z1 by A2,FDIFF_1:def 7;
reconsider x0 as Real by A11;
A14: ((u01(#)(x`|Z1) - v01(#)(y`|Z1)) | AB).x0
= (u01(#)(x`|Z1) - v01(#)(y`|Z1)).x0 by A10,FUNCT_1:47
.= (u01(#)(x`|Z1)).x0 - (v01(#)(y`|Z1)).x0 by A11,VALUED_1:13
.= u01.x0*(x`|Z1).x0 - (v01(#)(y`|Z1)).x0 by A12,VALUED_1:def 4
.= u01.x0*(x`|Z1).x0 - v01.x0*(y`|Z1).x0 by A12,VALUED_1:def 4
.= u01.x0*diff(x,x0) - v01.x0*(y`|Z1).x0 by A2,A13,FDIFF_1:def 7;
x0 in dom(u02(#)(x`|Z2) - v02(#)(y`|Z2)) /\ AB
by A8,A9,A10,RELAT_1:61;
then
A15: x0 in dom(u02(#)(x`|Z2) - v02(#)(y`|Z2)) by XBOOLE_0:def 4;
then
x0 in dom(u02(#)(x`|Z2)) /\ dom(v02(#)(y`|Z2)) by VALUED_1:12;
then
A16: x0 in dom(u02(#)(x`|Z2)) & x0 in dom(v02(#)(y`|Z2))
by XBOOLE_0:def 4;then
x0 in dom u02 /\ dom(x`|Z2) & x0 in dom v02 /\ dom(y`|Z2)
by VALUED_1:def 4;then
x0 in dom u02 & x0 in dom(x`|Z2)
& x0 in dom v02 & x0 in dom(y`|Z2) by XBOOLE_0:def 4;then
A17: x0 in Z2 by A1,FDIFF_1:def 7;
((u02(#)(x`|Z2) - v02(#)(y`|Z2)) | AB ).x0
= (u02(#)(x`|Z2) - v02(#)(y`|Z2)).x0 by A8,A9,A10,FUNCT_1:47
.= (u02(#)(x`|Z2)).x0 - (v02(#)(y`|Z2)).x0 by A15,VALUED_1:13
.= u02.x0*(x`|Z2).x0 - (v02(#)(y`|Z2)).x0 by A16,VALUED_1:def 4
.= u02.x0*(x`|Z2).x0 - v02.x0*(y`|Z2).x0 by A16,VALUED_1:def 4
.= u02.x0*diff(x,x0) - v02.x0*(y`|Z2).x0
by A1,A17,FDIFF_1:def 7; then
((u02(#)(x`|Z2) - v02(#)(y`|Z2)) | AB).x0
= u01.x0*diff(x,x0) - v01.x0*diff(y,x0)
by A1,A3,A4,A17,FDIFF_1:def 7;
hence thesis by A2,A13,A14,FDIFF_1:def 7;
end;
hence thesis by A8,A9,FUNCT_1:def 11;
end;
A18: integral( u01(#)(x`|Z1) - v01(#)(y`|Z1) ,a,b )
= integral( (u01(#)(x`|Z1) - v01(#)(y`|Z1)), AB ) by INTEGRA5:19
.= integral( u02(#)(x`|Z2) - v02(#)(y`|Z2) ,AB) by A5
.= integral( u02(#)(x`|Z2) - v02(#)(y`|Z2) ,a,b ) by INTEGRA5:19;
A19: (v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB
= (v02(#)(x`|Z2) + u02(#)(y`|Z2)) | AB
proof
dom(v01(#)(x`|Z1) + u01(#)(y`|Z1))
= dom(v01(#)(x`|Z1)) /\ dom(u01(#)(y`|Z1)) by VALUED_1:def 1
.= (dom v01 /\ dom(x`|Z1)) /\ dom(u01(#)(y`|Z1)) by VALUED_1:def 4
.= (dom v01 /\ dom(x`|Z1)) /\ (dom u01 /\ dom (y`|Z1))
by VALUED_1:def 4;then
A20: dom(v01(#)(x`|Z1) + u01(#)(y`|Z1))
= (dom v01 /\ Z1) /\ ( dom u01 /\ dom(y`|Z1)) by A2,FDIFF_1:def 7
.= (dom v01 /\ Z1) /\ ( dom u01 /\ Z1) by A2,FDIFF_1:def 7
.= dom v01 /\ (Z1 /\ ( dom u01 /\ Z1)) by XBOOLE_1:16
.= dom v01 /\ ((Z1 /\ Z1 ) /\ dom u01) by XBOOLE_1:16
.= (dom v01 /\ dom u01) /\ Z1 by XBOOLE_1:16;
dom(v02(#)(x`|Z2) + u02(#)(y`|Z2))
= dom(v02(#)(x`|Z2)) /\ dom(u02(#)(y`|Z2)) by VALUED_1:def 1
.= (dom v02 /\ dom(x`|Z2)) /\ dom(u02(#)(y`|Z2)) by VALUED_1:def 4
.= (dom v02 /\ dom(x`|Z2)) /\ (dom u02 /\ dom (y`|Z2))
by VALUED_1:def 4;then
A21: dom(v02(#)(x`|Z2) + u02(#)(y`|Z2))
= (dom v02 /\ Z2) /\ ( dom u02 /\ dom(y`|Z2)) by A1,FDIFF_1:def 7
.= (dom v02 /\ Z2) /\ ( dom u02 /\ Z2) by A1,FDIFF_1:def 7
.= dom v02 /\ (Z2 /\ ( dom u02 /\ Z2)) by XBOOLE_1:16
.= dom v02 /\ ((Z2 /\ Z2 ) /\ dom u02) by XBOOLE_1:16
.= (dom v01 /\ dom u01) /\ Z2 by A3,A4,XBOOLE_1:16;
A22: dom((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB)
= dom (v01(#)(x`|Z1) + u01(#)(y`|Z1)) /\ AB by RELAT_1:61
.= (dom v01 /\ dom u01) /\ (Z1 /\ AB) by A20,XBOOLE_1:16
.= (dom v01 /\ dom u01) /\ AB by A1,XBOOLE_1:28;
A23: dom((v02(#)(x`|Z2) + u02(#)(y`|Z2)) | AB)
= dom (v02(#)(x`|Z2) + u02(#)(y`|Z2)) /\ AB by RELAT_1:61
.= (dom v01 /\ dom u01) /\ (Z2 /\ AB) by A21,XBOOLE_1:16
.= (dom v01 /\ dom u01) /\ AB by A1,XBOOLE_1:1,28;
for x0 being object st x0 in dom((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB )
holds
((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB).x0
= ((v02(#)(x`|Z2) + u02(#)(y`|Z2)) | AB).x0
proof
let x0 being object such that
A24: x0 in dom((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB );
x0 in dom(v01(#)(x`|Z1) + u01(#)(y`|Z1)) /\ AB by A24,RELAT_1:61;
then
A25: x0 in dom(v01(#)(x`|Z1) + u01(#)(y`|Z1)) by XBOOLE_0:def 4;
then
x0 in dom(v01(#)(x`|Z1)) /\ dom(u01(#)(y`|Z1)) by VALUED_1:def 1;
then
A26: x0 in dom(v01(#)(x`|Z1)) & x0 in dom(u01(#)(y`|Z1))
by XBOOLE_0:def 4;then
A27: x0 in dom v01 /\ dom(x`|Z1) & x0 in dom u01 /\ dom(y`|Z1)
by VALUED_1:def 4;then
x0 in dom v01 & x0 in dom(x`|Z1)
& x0 in dom u01 & x0 in dom(y`|Z1) by XBOOLE_0:def 4; then
A28: x0 in Z1 by A2,FDIFF_1:def 7;
reconsider x0 as Real by A27;
((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB).x0
= (v01(#)(x`|Z1) + u01(#)(y`|Z1)).x0 by A24,FUNCT_1:47
.= (v01(#)(x`|Z1)).x0 + (u01(#)(y`|Z1)).x0 by A25,VALUED_1:def 1
.= v01.x0*(x`|Z1).x0 + (u01(#)(y`|Z1)).x0 by A26,VALUED_1:def 4
.= v01.x0*(x`|Z1).x0 + u01.x0*(y`|Z1).x0 by A26,VALUED_1:def 4
.= v01.x0*diff(x,x0) + u01.x0*(y`|Z1).x0
by A2,A28,FDIFF_1:def 7; then
A29: ((v01(#)(x`|Z1) + u01(#)(y`|Z1)) | AB).x0
= v01.x0*diff(x,x0) + u01.x0*diff(y,x0)
by A2,A28,FDIFF_1:def 7;
x0 in dom(v02(#)(x`|Z2) + u02(#)(y`|Z2)) /\ AB
by A22,A23,A24,RELAT_1:61; then
A30: x0 in dom(v02(#)(x`|Z2) + u02(#)(y`|Z2)) by XBOOLE_0:def 4;
then
x0 in dom(v02(#)(x`|Z2)) /\ dom(u02(#)(y`|Z2)) by VALUED_1:def 1;
then
A31: x0 in dom(v02(#)(x`|Z2)) & x0 in dom(u02(#)(y`|Z2))
by XBOOLE_0:def 4;then
x0 in dom v02 /\ dom(x`|Z2) & x0 in dom u02 /\ dom(y`|Z2)
by VALUED_1:def 4;then
x0 in dom v02 & x0 in dom(x`|Z2)
& x0 in dom u02 & x0 in dom(y`|Z2) by XBOOLE_0:def 4;then
A32: x0 in Z2 by A1,FDIFF_1:def 7;
((v02(#)(x`|Z2) + u02(#)(y`|Z2)) | AB ).x0
= (v02(#)(x`|Z2) + u02(#)(y`|Z2)).x0 by A22,A23,A24,FUNCT_1:47
.= (v02(#)(x`|Z2)).x0 + (u02(#)(y`|Z2)).x0 by A30,VALUED_1:def 1
.= v02.x0*(x`|Z2).x0 + (u02(#)(y`|Z2)).x0 by A31,VALUED_1:def 4
.= v02.x0*(x`|Z2).x0 + u02.x0*(y`|Z2).x0 by A31,VALUED_1:def 4
.= v02.x0*diff(x,x0) + u02.x0*(y`|Z2).x0
by A1,A32,FDIFF_1:def 7;
hence thesis by A1,A3,A4,A29,A32,FDIFF_1:def 7;
end;
hence thesis by A22,A23,FUNCT_1:def 11;
end;
integral( v01(#)(x`|Z1) + u01(#)(y`|Z1),a,b)
= integral( v01(#)(x`|Z1) + u01(#)(y`|Z1),AB) by INTEGRA5:19
.= integral( (v02(#)(x`|Z2) + u02(#)(y`|Z2)),AB) by A19
.=integral( v02(#)(x`|Z2) + u02(#)(y`|Z2) ,a,b) by INTEGRA5:19;
hence thesis by A3,A4,A18;
end;
Lm2: for a,b be Real, x1,y1,x2,y2 be PartFunc of REAL,REAL,
Z be Subset of REAL,
f be PartFunc of COMPLEX,COMPLEX st
a <= b &
[.a,b.] c= dom x1 & [.a,b.] c= dom y1 &
[.a,b.] c= dom x2 & [.a,b.] c= dom y2 &
x1| [.a,b.] = x2| [.a,b.] & y1| [.a,b.] = y2| [.a,b.] & Z is open &
[.a,b.] c= Z & x1 is_differentiable_on Z & y1 is_differentiable_on Z &
rng ( (x1 + <i>(#)y1) | [.a,b.] ) c=dom f &
x2 is_differentiable_on Z & y2 is_differentiable_on Z &
rng ( (x2 + <i>(#)y2) | [.a,b.] ) c=dom f
holds
integral(f,x1,y1,a,b,Z) = integral(f,x2,y2,a,b,Z)
proof
let a,b be Real,
x1,y1,x2,y2 be PartFunc of REAL,REAL,
Z be Subset of REAL,
f be PartFunc of COMPLEX, COMPLEX;
assume
A1: a <= b & [.a,b.] c= dom x1 & [.a,b.] c= dom y1 &
[.a,b.] c= dom x2 & [.a,b.] c= dom y2 &
x1| [.a,b.] = x2| [.a,b.] & y1| [.a,b.] = y2| [.a,b.] &
Z is open & [.a,b.] c= Z & x1 is_differentiable_on Z &
y1 is_differentiable_on Z &
rng ( (x1 + <i>(#)y1) | [.a,b.] ) c= dom f &
x2 is_differentiable_on Z & y2 is_differentiable_on Z &
rng ( (x2 + <i>(#)y2) | [.a,b.] ) c=dom f;
consider u01, v01 be PartFunc of REAL,REAL such that
A2: u01=(Re f)* (R2-to-C) *<:x1,y1:> & v01=(Im f)* (R2-to-C) *<:x1,y1:> &
integral(f,x1,y1,a,b,Z)= integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,a,b )
+ integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,a,b )*<i> by Def2;
consider u02,v02 be PartFunc of REAL,REAL such that
A3: u02=(Re f)* (R2-to-C) *<:x2,y2:> & v02=(Im f)* (R2-to-C) *<:x2,y2:> &
integral(f,x2,y2,a,b,Z)= integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,a,b )
+ integral( v02(#)(x2`|Z) + u02(#)(y2`|Z) ,a,b )*<i> by Def2;
reconsider AB=[.a,b.] as non empty closed_interval Subset of REAL
by A1,MEASURE5:14;
A4: now assume
A5: not (a = b or a < b);then
0 < b - a or 0 < a - b by XREAL_1:55;then
a < a + (b -a) or 0 < a - b by XREAL_1:29;then
a < b or b < b + (a - b) by XREAL_1:29;
hence contradiction by A5,A1;
end;
per cases by A4;
suppose
A6: a < b;
A7: u01 | AB = u02 | AB
proof
A8: dom(u01 | AB) = dom(u02 | AB)
proof
A9: for x0 be object st x0 in dom(u01 | AB) holds x0 in dom(u02 | AB)
proof
let x0 be object such that
A10: x0 in dom(u01 | AB);
x0 in dom u01 /\ AB by A10,RELAT_1:61;then
A11: x0 in dom u01 & x0 in AB by XBOOLE_0:def 4;then
x0 in dom <:x1,y1:> & <:x1,y1:>.x0 in dom((Re f)* (R2-to-C))
& x0 in AB by A2,FUNCT_1:11;then
x0 in AB &
[x1.x0,y1.x0] in dom((Re f)* (R2-to-C)) by FUNCT_3:def 7; then
x0 in AB &
[(x1 | AB).x0,y1.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:49;
then
x0 in AB & [(x2 | AB).x0,(y2 | AB).x0] in dom((Re f)* (R2-to-C))
by A1,FUNCT_1:49;then
x0 in AB & [(x2 | AB).x0,y2.x0] in dom((Re f)* (R2-to-C))
by FUNCT_1:49; then
A12: x0 in AB & [x2.x0,y2.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:49;
x0 in dom x2 /\ dom y2 by A1,A11,XBOOLE_0:def 4;then
x0 in dom <:x2,y2:> by FUNCT_3:def 7;then
x0 in AB & x0 in dom <:x2,y2:>
& <:x2,y2:>.x0 in dom((Re f)* (R2-to-C))
by A12,FUNCT_3:def 7;then
x0 in AB & x0 in dom u02 by A3,FUNCT_1:11;then
x0 in dom u02 /\ AB by XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
for x0 be object st x0 in dom(u02 | AB) holds x0 in dom(u01 | AB)
proof
let x0 be object such that
A13: x0 in dom(u02 | AB);
x0 in dom u02 /\ AB by A13,RELAT_1:61;then
A14: x0 in dom u02 & x0 in AB by XBOOLE_0:def 4;then
x0 in dom <:x2,y2:> & <:x2,y2:>.x0 in dom((Re f)* (R2-to-C))
& x0 in AB by A3,FUNCT_1:11;then
x0 in AB & [x2.x0,y2.x0] in dom((Re f)* (R2-to-C)) by FUNCT_3:def 7;
then
x0 in AB &
[(x2 | AB).x0,y2.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:49;
then
x0 in AB & [(x1 | AB).x0,(y1 | AB).x0] in dom((Re f)* (R2-to-C))
by A1,FUNCT_1:49;then
x0 in AB & [(x1 | AB).x0,y1.x0] in dom((Re f)* (R2-to-C))
by FUNCT_1:49;then
A15: x0 in AB & [x1.x0,y1.x0] in dom((Re f)* (R2-to-C)) by FUNCT_1:49;
x0 in dom x1 /\ dom y1 by A1,A14,XBOOLE_0:def 4;then
x0 in dom <:x1,y1:> by FUNCT_3:def 7;then
x0 in AB & x0 in dom <:x1,y1:> &
<:x1,y1:>.x0 in dom((Re f)* (R2-to-C))
by A15,FUNCT_3:def 7;then
x0 in AB & x0 in dom u01 by A2,FUNCT_1:11;then
x0 in dom u01 /\ AB by XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
hence thesis by A9,TARSKI:2;
end;
for x0 be object st x0 in dom(u01 | AB)
holds (u01 | AB).x0 = (u02 | AB).x0
proof
let x0 be object such that
A16: x0 in dom(u01 | AB);
x0 in dom u01 /\ AB by A16,RELAT_1:61;
then
A17: x0 in AB & x0 in dom u01 by XBOOLE_0:def 4;
then reconsider x0 as Real;
A18: AB c= dom x1 /\ dom y1 by A1,XBOOLE_1:19;then
x0 in dom x1 /\ dom y1 by A17;then
x0 in dom (<:x1,y1:>) by FUNCT_3:def 7;then
A19: u01.x0 = ((Re f)*(R2-to-C)).(<:x1,y1:>.x0) by A2,FUNCT_1:13;
A20: AB c= dom x2 /\ dom y2 by A1,XBOOLE_1:19;then
x0 in dom x2 /\ dom y2 by A17;then
x0 in dom (<:x2,y2:>) by FUNCT_3:def 7;then
u02.x0 = ((Re f)*(R2-to-C)).(<:x2,y2:>.x0) by A3,FUNCT_1:13;
then
A21: u02.x0 = ((Re f)*(R2-to-C)).([x2.x0,y2.x0]) by A17,A20,FUNCT_3:48;
A22: x1.x0 = (x1| [.a,b.]).x0 by A17,FUNCT_1:49
.= x2.x0 by A17,A1,FUNCT_1:49;
A23: y1.x0 = (y1| [.a,b.]).x0 by A17,FUNCT_1:49
.= y2.x0 by A17,A1,FUNCT_1:49;
u01.x0 = (u01 | AB).x0 & u02.x0 = (u02 | AB).x0 by A17,FUNCT_1:49;
hence thesis by A17,A18,A19,A21,A22,A23,FUNCT_3:48;
end;
hence thesis by A8,FUNCT_1:def 11;
end;
A24: (x1`|Z)| AB = (x2`|Z)| AB
proof
A25: dom ((x1`|Z)| AB) = dom (x1`|Z) /\ AB by RELAT_1:61
.= Z /\ AB by A1,FDIFF_1:def 7
.= AB by A1,XBOOLE_1:28;
A26: dom ((x2`|Z)| AB) = dom (x2`|Z) /\ AB by RELAT_1:61
.= Z /\ AB by A1,FDIFF_1:def 7
.= AB by A1,XBOOLE_1:28;
for x0 be object st x0 in dom((x1`|Z)| AB) holds
((x1`|Z)| AB).x0 = ((x2`|Z)| AB).x0
proof
let x0 be object such that
A27: x0 in dom((x1`|Z)| AB);
x0 in dom(x1`|Z) by A27,RELAT_1:57;
then reconsider x0 as Real;
A28: ((x2`|Z)| AB).x0 = (x2`|Z).x0 by A27,FUNCT_1:49;
A29: (x1`|Z).x0 = diff(x1,x0) by A1,A25,A27,FDIFF_1:def 7;
A30: (x2`|Z).x0 = diff(x2,x0) by A1,A25,A27,FDIFF_1:def 7;
A31: now assume
A32: not (x0 in ].a,b.[ or x0 = a or x0 = b);
x0 in {r where r is Real: a <= r & r <= b}
by A25,A27,RCOMP_1:def 1;then
A33: ex r be Real st r = x0 & a <= r & r <= b;
A34: now assume
A35: not (a = x0 or a < x0);then
0 < x0 - a or 0 < a - x0 by XREAL_1:55;then
a < a + (x0 -a) or 0 < a - x0 by XREAL_1:29;then
a < x0 or x0 < x0 + (a - x0) by XREAL_1:29;
hence contradiction by A33,A35;
end;
A36: now assume
A37: not (x0 = b or x0 < b);then
0 < x0 - b or 0 < b - x0 by XREAL_1:55;then
b < b + (x0 -b) or 0 < b - x0 by XREAL_1:29;then
b < x0 or x0 < x0 + (b - x0) by XREAL_1:29;
hence contradiction by A33,A37;
end;
not (x0 in {q where q is Real: a<q & q<b})
by A32,RCOMP_1:def 2;
hence contradiction by A32,A34,A36;
end;
diff(x1,x0) = diff(x2,x0)
proof
per cases by A31;
suppose
A38: x0 = a;
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,c1 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,c1 such that
A45: rng c1 = {x0} & rng (h+c1) c= dom (x1-x2) &
(for n being Nat holds h.n > 0);
A46: h is convergent & lim h = 0;
A47: 0 < b - x0 by A6,A38,XREAL_1:50;
then consider n 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 st 0<p1 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 such that
A50: 0 < p1;
take n;
for m being Nat st n <= m holds
(h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m = 0
proof
let m be Nat such that
A51: n <= m;
A52: m in NAT by ORDINAL1:def 12;
A53: |.h.m - 0 .| < (b - x0)/2 by A48,A51;
A54: 0 < h.m by A45;then
A55: h.m < (b - x0)/2 by A53,ABSVALUE:def 1;
A56: a + 0 <= x0 + h.m by A38,A54,XREAL_1:7;
x0 + h.m <= x0 + (b - x0)/2 by A55,XREAL_1:7;then
A57: x0 + h.m + 0 <= b - (b - x0)/2 + (b - x0)/2
by A47,XREAL_1:7;
A58: [.a,b.] c= dom x1 /\ dom x2 by A1,XBOOLE_1:19;then
x0 in dom x1 /\ dom x2 by A39;then
A59: x0 in dom(x1-x2) by VALUED_1:12;
A60: [.a,b.] c= dom(x1-x2) by A58,VALUED_1:12;
x0 + h.m in {r where r 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 thesis by A66,A67;
end;
hence thesis by A50,COMPLEX1:44;
end;
then (h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1))
is convergent by SEQ_2:def 6;
hence thesis by A49,SEQ_2:def 7;
end;then
Rdiff(x1,x0) - Rdiff(x2,x0) = 0 by A43,A44,FDIFF_3:def 6;
hence thesis;
end;
hence thesis by A40,A42,FDIFF_3:22;
end;
suppose
A68: x0 in ].a,b.[;
A69: ].a,b.[ is open by RCOMP_1:7;
A70: ].a,b.[ c= [.a,b.]
proof
for x0 be object st x0 in ].a,b.[ holds x0 in [.a,b.]
proof
let x0 be object such that
A71: x0 in ].a,b.[;
x0 in {r where r is Real : a < r & r < b }
by A71,RCOMP_1:def 2;then
A72: ex r st r=x0 & a < r & r < b;then
reconsider x0 as Real;
x0 in {r where r is Real : a <= r & r <= b } by A72;
hence thesis by RCOMP_1:def 1;
end;
hence thesis;
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,28
.= dom x2 /\ (].a,b.[) by A1,A70,XBOOLE_1:1,28
.= dom (x2| (].a,b.[) ) by RELAT_1:61;
for x0 be object st x0 in dom (x1| (].a,b.[) ) holds
(x1| (].a,b.[) ).x0 = (x2| (].a,b.[) ).x0
proof
let x0 be object such that
A80: x0 in dom (x1| (].a,b.[) );
A81: dom (x1| (].a,b.[) ) = dom x1 /\ (].a,b.[) by RELAT_1:61
.= ].a,b.[ by A1,A70,XBOOLE_1:1,28;
then (x1| (].a,b.[) ).x0 = x1.x0 by A80,FUNCT_1:49
.= (x1| ([.a,b.]) ).x0 by A70,A80,A81,FUNCT_1:49
.= x2.x0 by A70,A80,A81,A1,FUNCT_1:49
.=(x2| (].a,b.[) ).x0 by A80,A81,FUNCT_1:49;
hence thesis;
end;
hence thesis by A74,A75,A77,A78,A79,FUNCT_1:2;
end;
suppose
A82: x0 = b;
then x0 in {r where r 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,c1 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,c1 such that
A89: rng c1 = {x0} & rng (h+c1) c= dom (x1-x2) &
(for n being Nat holds h.n < 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 st 0<p1
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 such that
A94: 0 < p1;
take n;
for m being Nat st n <= m holds
(h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1)).m = 0
proof
let m being Nat such that
A95: n <= m;
A96: m in NAT by ORDINAL1:def 12;
A97: |.h.m - 0 .| < (x0 - a)/2 by A92,A95;
A98: h.m < 0 by A89;then
A99: -h.m < (x0 - a)/2 by A97,ABSVALUE:def 1;
A100: x0 + h.m <= b + 0 by A82,A98,XREAL_1:7;
x0 - (x0 - a)/2 <= x0 - (-h.m) by A99,XREAL_1:13;then
A101: a + (x0 - a)/2 - (x0 - a)/2 <= x0 + h.m - 0
by A82,A91,XREAL_1:13;
A102: [.a,b.] c= dom x1 /\ dom x2 by A1,XBOOLE_1:19;then
x0 in dom x1 /\ dom x2 by A83;then
A103: x0 in dom(x1-x2) by VALUED_1:12;
A104: [.a,b.] c= dom(x1-x2) by A102,VALUED_1:12;
x0 + h.m in {r where r 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 thesis by A109,A110;
end;
hence thesis by A94,COMPLEX1:44;
end; then
(h"(#)((x1-x2)/*(h+c1) - (x1-x2)/*c1))
is convergent by SEQ_2:def 6;
hence thesis by A93,SEQ_2:def 7;
end;then
Ldiff(x1-x2,x0) = 0 by A87,FDIFF_3:def 5;
hence thesis by A88;
end;
hence thesis by A84,A86,FDIFF_3:22;
end;
end;
hence thesis by A27,A28,A29,A30,FUNCT_1:49;
end;
hence thesis by A25,A26,FUNCT_1:def 11;
end;
A111: v01 | AB = v02 | AB
proof
A112: dom(v01 | AB) = dom(v02 | AB)
proof
A113: for x0 be object st x0 in dom(v01 | AB) holds x0 in dom(v02 | AB)
proof
let x0 be object such that
A114: x0 in dom(v01 | AB);
x0 in dom v01 /\ AB by A114,RELAT_1:61;then
A115: x0 in dom v01 & x0 in AB by XBOOLE_0:def 4;then
x0 in dom <:x1,y1:> & <:x1,y1:>.x0 in dom((Im f)* (R2-to-C)) &
x0 in AB by A2,FUNCT_1:11;then
x0 in AB &
[x1.x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_3:def 7;then
x0 in AB &
[(x1 | AB).x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:49;
then
x0 in AB & [(x2 | AB).x0,(y2 | AB).x0] in dom((Im f)* (R2-to-C))
by A1,FUNCT_1:49;then
x0 in AB &
[(x2 | AB).x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:49;
then
A116: x0 in AB & [x2.x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:49;
x0 in dom x2 /\ dom y2 by A1,A115,XBOOLE_0:def 4;then
x0 in dom <:x2,y2:> by FUNCT_3:def 7;then
x0 in AB & x0 in dom <:x2,y2:> &
<:x2,y2:>.x0 in dom((Im f)* (R2-to-C))
by A116,FUNCT_3:def 7;then
x0 in AB & x0 in dom v02 by A3,FUNCT_1:11;then
x0 in dom v02 /\ AB by XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
for x0 be object st x0 in dom(v02 | AB) holds x0 in dom(v01 | AB)
proof
let x0 be object such that
A117: x0 in dom(v02 | AB);
x0 in dom v02 /\ AB by A117,RELAT_1:61;then
A118: x0 in dom v02 & x0 in AB by XBOOLE_0:def 4;then
x0 in dom <:x2,y2:> & <:x2,y2:>.x0 in dom((Im f)* (R2-to-C)) &
x0 in AB by A3,FUNCT_1:11;then
x0 in AB &
[x2.x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_3:def 7;then
x0 in AB &
[(x2 | AB).x0,y2.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:49;
then x0 in AB & [(x1 | AB).x0,(y1 | AB).x0] in dom((Im f)* (R2-to-C))
by A1,FUNCT_1:49;then
x0 in AB &
[(x1 | AB).x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:49;
then
A119: x0 in AB & [x1.x0,y1.x0] in dom((Im f)* (R2-to-C)) by FUNCT_1:49;
x0 in dom x1 /\ dom y1 by A1,A118,XBOOLE_0:def 4;then
x0 in dom <:x1,y1:> by FUNCT_3:def 7;then
x0 in AB & x0 in dom <:x1,y1:> &
<:x1,y1:>.x0 in dom((Im f)* (R2-to-C))
by A119,FUNCT_3:def 7;then
x0 in AB & x0 in dom v01 by A2,FUNCT_1:11;then
x0 in dom v01 /\ AB by XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
hence thesis by A113,TARSKI:2;
end;
for x0 be object st x0 in dom(v01 | AB)
holds (v01 | AB).x0 = (v02 | AB).x0
proof
let x0 be object such that
A120: x0 in dom(v01 | AB);
x0 in dom v01 /\ AB by A120,RELAT_1:61;
then
A121: x0 in AB & x0 in dom v01 by XBOOLE_0:def 4;
then reconsider x0 as Real;
A122: AB c= dom x1 /\ dom y1 by A1,XBOOLE_1:19;then
x0 in dom x1 /\ dom y1 by A121;then
x0 in dom (<:x1,y1:>) by FUNCT_3:def 7;then
A123: v01.x0 = ((Im f)*(R2-to-C)).(<:x1,y1:>.x0) by A2,FUNCT_1:13;
A124: AB c= dom x2 /\ dom y2 by A1,XBOOLE_1:19;then
x0 in dom x2 /\ dom y2 by A121;then
x0 in dom (<:x2,y2:>) by FUNCT_3:def 7;then
v02.x0 = ((Im f)*(R2-to-C)).(<:x2,y2:>.x0) by A3,FUNCT_1:13;then
A125: v02.x0 = ((Im f)*(R2-to-C)).([x2.x0,y2.x0]) by A121,A124,FUNCT_3:48;
A126: x1.x0 = (x1| [.a,b.]).x0 by A121,FUNCT_1:49
.= x2.x0 by A121,A1,FUNCT_1:49;
A127: y1.x0 = (y1| [.a,b.]).x0 by A121,FUNCT_1:49
.= y2.x0 by A121,A1,FUNCT_1:49;
v01.x0 = (v01 | AB).x0 & v02.x0 = (v02 | AB).x0 by A121,FUNCT_1:49;
hence thesis by A126,A127,A123,A121,A122,A125,FUNCT_3:48;
end;
hence thesis by A112,FUNCT_1:def 11;
end;
A128: (y1`|Z)| AB = (y2`|Z)| AB
proof
A129: dom ((y1`|Z)| AB) = dom (y1`|Z) /\ AB by RELAT_1:61
.= Z /\ AB by A1,FDIFF_1:def 7
.= AB by A1,XBOOLE_1:28;
A130: dom ((y2`|Z)| AB) = dom (y2`|Z) /\ AB by RELAT_1:61
.= Z /\ AB by A1,FDIFF_1:def 7
.= AB by A1,XBOOLE_1:28;
for x0 be object st x0 in dom((y1`|Z)| AB) holds
((y1`|Z)| AB).x0 = ((y2`|Z)| AB).x0
proof
let x0 be object such that
A131: x0 in dom((y1`|Z)| AB);
x0 in dom(y1`|Z) by A131,RELAT_1:57;
then reconsider x0 as Real;
A132: ((y2`|Z)| AB).x0 = (y2`|Z).x0 by A131,FUNCT_1:49;
A133: (y1`|Z).x0 = diff(y1,x0) by A1,A131,A129,FDIFF_1:def 7;
A134: (y2`|Z).x0 = diff(y2,x0) by A1,A131,A129,FDIFF_1:def 7;
A135: now assume
A136: not (x0 in ].a,b.[ or x0 = a or x0 = b);
x0 in {r where r is Real: a <= r & r <= b}
by A129,A131,RCOMP_1:def 1;then
A137: ex r be Real st r=x0 & a<=r & r<=b;
A138: now assume
A139: not (a = x0 or a < x0);then
0 < x0 - a or 0 < a - x0 by XREAL_1:55;then
a < a + (x0 -a) or 0 < a - x0 by XREAL_1:29;then
a < x0 or x0 < x0 + (a - x0) by XREAL_1:29;
hence contradiction by A137,A139;
end;
A140: now assume
A141: not (x0 = b or x0 < b);then
0 < x0 - b or 0 < b - x0 by XREAL_1:55;then
b < b + (x0 -b) or 0 < b - x0 by XREAL_1:29;then
b < x0 or x0 < x0 + (b - x0) by XREAL_1:29;
hence contradiction by A137,A141;
end;
not (x0 in {q where q is Real: a<q & q<b})
by A136,RCOMP_1:def 2;
hence contradiction by A136,A138,A140;
end;
diff(y1,x0) = diff(y2,x0)
proof
per cases by A135;
suppose
A142: x0 = a;
then x0 in {r where r 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,c1 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,c1 such that
A149: rng c1 = {x0} & rng (h+c1) c= dom (y1-y2) &
(for n being Nat holds h.n > 0);
A150: h is convergent & lim h = 0;
A151: 0 < b - x0 by A6,A142,XREAL_1:50;
then consider n 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 st 0 < p1
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 such that
A154: 0 < p1;
take n;
for m being Nat st n <= m holds
(h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m = 0
proof
let m be Nat such that
A155: n <= m;
A156: |.h.m - 0 .| < (b - x0)/2 by A152,A155;
A157: m in NAT by ORDINAL1:def 12;
A158: 0 < h.m by A149;then
A159: h.m < (b - x0)/2 by A156,ABSVALUE:def 1;
A160: a + 0 <= x0 + h.m by A142,A158,XREAL_1:7;
x0 + h.m <= x0 + (b - x0)/2 by A159,XREAL_1:7;then
A161: x0 + h.m + 0 <= b - (b - x0)/2 + (b - x0)/2
by A151,XREAL_1:7;
A162: [.a,b.] c= dom y1 /\ dom y2 by A1,XBOOLE_1:19;then
x0 in dom y1 /\ dom y2 by A143;then
A163: x0 in dom(y1-y2) by VALUED_1:12;
A164: [.a,b.] c= dom(y1-y2) by A162,VALUED_1:12;
x0 + h.m in {r where r 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 thesis by A170,A171;
end;
hence thesis by A154,COMPLEX1:44;
end;
then (h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1))
is convergent by SEQ_2:def 6;
hence thesis by A153,SEQ_2:def 7;
end;then
Rdiff(y1,x0) - Rdiff(y2,x0) = 0 by A147,A148,FDIFF_3:def 6;
hence thesis;
end;
hence thesis by A144,A146,FDIFF_3:22;
end;
suppose
A172: x0 in ].a,b.[;
A173: ].a,b.[ is open by RCOMP_1:7;
A174: ].a,b.[ c= [.a,b.]
proof
for x0 be object st x0 in ].a,b.[ holds x0 in [.a,b.]
proof
let x0 be object such that
A175: x0 in ].a,b.[;
x0 in {r where r is Real: a < r & r < b }
by A175,RCOMP_1:def 2;then
A176: ex r st r = x0 & a < r & r < b;then
reconsider x0 as Real;
x0 in {r where r is Real: a <= r & r <= b } by A176;
hence thesis by RCOMP_1:def 1;
end;
hence thesis;
end;then
A177: y1 is_differentiable_on ].a,b.[ by A1,A173,FDIFF_1:26,XBOOLE_1:1;
then
A178: y1| (].a,b.[) is_differentiable_on ].a,b.[ &
(y1| (].a,b.[))`| (].a,b.[) = y1`| (].a,b.[) by 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,28
.= dom y2 /\ (].a,b.[) by A1,A174,XBOOLE_1:1,28
.= dom (y2| (].a,b.[) ) by RELAT_1:61;
for x0 be object st x0 in dom (y1| (].a,b.[) ) holds
(y1| (].a,b.[) ).x0 = (y2| (].a,b.[) ).x0
proof
let x0 be object such that
A184: x0 in dom (y1| (].a,b.[) );
A185: dom (y1| (].a,b.[) ) = dom y1 /\ (].a,b.[) by RELAT_1:61
.= ].a,b.[ by A1,A174,XBOOLE_1:1,28;
then (y1| (].a,b.[) ).x0 = y1.x0 by A184,FUNCT_1:49
.= (y1| ([.a,b.]) ).x0 by A174,A184,A185,FUNCT_1:49
.= y2.x0 by A174,A184,A185,A1,FUNCT_1:49
.= (y2| (].a,b.[) ).x0 by A184,A185,FUNCT_1:49;
hence thesis;
end;
hence thesis by A178,A179,A181,A182,A183,FUNCT_1:2;
end;
suppose
A186: x0 = b;
then x0 in {r where r 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,c1 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,c1 such that
A193: rng c1 = {x0} & rng (h+c1) c= dom (y1-y2) &
(for n being Nat holds h.n < 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 st 0 < p1
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 such that
A198: 0 < p1;
take n;
for m being Nat st n <= m holds
(h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1)).m = 0
proof
let m be Nat such that
A199: n <= m;
A200: |.h.m - 0 .| < (x0 - a)/2 by A196,A199;
A201: m in NAT by ORDINAL1:def 12;
A202: h.m < 0 by A193;then
A203: -h.m < (x0 - a)/2 by A200,ABSVALUE:def 1;
A204: x0 + h.m <= b + 0 by A186,A202,XREAL_1:7;
x0 - (x0 - a)/2 <= x0 - (-h.m) by A203,XREAL_1:13;
then
A205: a + (x0 - a)/2 - (x0 - a)/2 <= x0 + h.m - 0
by A186,A195,XREAL_1:13;
A206: [.a,b.] c= dom y1 /\ dom y2 by A1,XBOOLE_1:19;then
x0 in dom y1 /\ dom y2 by A187;then
A207: x0 in dom(y1-y2) by VALUED_1:12;
A208: [.a,b.] c= dom(y1-y2) by A206,VALUED_1:12;
x0 + h.m in {r where r 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 thesis by A213,A214;
end;
hence thesis by A198,COMPLEX1:44;
end; then
(h"(#)((y1-y2)/*(h+c1) - (y1-y2)/*c1))
is convergent by SEQ_2:def 6;
hence thesis by A197,SEQ_2:def 7;
end;then
Ldiff(y1-y2,x0) = 0 by A191,FDIFF_3:def 5;
hence thesis by A192;
end;
hence thesis by A188,A190,FDIFF_3:22;
end;
end;
hence thesis by A131,A132,A133,A134,FUNCT_1:49;
end;
hence thesis by A129,A130,FUNCT_1:def 11;
end;
A215: (u01(#)(x1`|Z) - v01(#)(y1`|Z)) | AB
= (u02(#)(x2`|Z) - v02(#)(y2`|Z)) | AB
proof
A216: x1`|Z is PartFunc of REAL,COMPLEX & y1`|Z is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7;
A217: u01 is PartFunc of REAL,COMPLEX & v01 is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7;
u01(#)(x1`|Z) is PartFunc of REAL,COMPLEX &
v01(#)(y1`|Z) is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7;then
A218: (u01(#)(x1`|Z) - v01(#)(y1`|Z)) | AB
= (u01(#)(x1`|Z)) | AB - (v01(#)(y1`|Z)) | AB by CFUNCT_1:55
.= (u01| AB)(#)((x1`|Z)| AB) - (v01(#)(y1`|Z)) | AB
by A216,A217,CFUNCT_1:53
.= (u01| AB)(#)((x1`|Z)| AB) - (v01| AB)(#)((y1`|Z)| AB)
by A216,A217,CFUNCT_1:53;
A219: x2`|Z is PartFunc of REAL,COMPLEX & y2`|Z is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7;
A220: u02 is PartFunc of REAL,COMPLEX & v02 is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7;
u02(#)(x2`|Z) is PartFunc of REAL,COMPLEX &
v02(#)(y2`|Z) is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7;
then
(u02(#)(x2`|Z) - v02(#)(y2`|Z)) | AB
= (u02(#)(x2`|Z)) | AB - (v02(#)(y2`|Z)) | AB by CFUNCT_1:55
.= (u02| AB)(#)((x2`|Z)| AB) - (v02(#)(y2`|Z)) | AB
by A219,A220,CFUNCT_1:53
.= (u02| AB)(#)((x2`|Z)| AB) - (v02| AB)(#)((y2`|Z)| AB)
by A219,A220,CFUNCT_1:53;
hence thesis by A7,A24,A111,A128,A218;
end;
A221: integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,a,b )
= integral( (u01(#)(x1`|Z) - v01(#)(y1`|Z)), AB ) by INTEGRA5:19
.= integral( u02(#)(x2`|Z) - v02(#)(y2`|Z),AB) by A215
.= integral( u02(#)(x2`|Z) - v02(#)(y2`|Z),a,b ) by INTEGRA5:19;
A222: (v01(#)(x1`|Z) + u01(#)(y1`|Z)) | AB
= (v02(#)(x2`|Z) + u02(#)(y2`|Z)) | AB
proof
A223: x1`|Z is PartFunc of REAL,COMPLEX &
y1`|Z is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:7;
A224: v01 is PartFunc of REAL,COMPLEX &
u01 is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:7;
v01(#)(x1`|Z) is PartFunc of REAL,COMPLEX &
u01(#)(y1`|Z) is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7;
then
A225: (v01(#)(x1`|Z) + u01(#)(y1`|Z)) | AB
= (v01(#)(x1`|Z)) | AB + (u01(#)(y1`|Z)) | AB by CFUNCT_1:52
.= (v01| AB)(#)((x1`|Z)| AB) + (u01(#)(y1`|Z)) | AB
by A223,A224,CFUNCT_1:53
.= (v01| AB)(#)((x1`|Z)| AB) + (u01| AB)(#)((y1`|Z)| AB)
by A223,A224,CFUNCT_1:53;
A226: x2`|Z is PartFunc of REAL,COMPLEX &
y2`|Z is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:7;
A227: v02 is PartFunc of REAL,COMPLEX &
u02 is PartFunc of REAL,COMPLEX by NUMBERS:11,RELSET_1:7;
v02(#)(x2`|Z) is PartFunc of REAL,COMPLEX &
u02(#)(y2`|Z) is PartFunc of REAL,COMPLEX
by NUMBERS:11,RELSET_1:7; then
(v02(#)(x2`|Z) + u02(#)(y2`|Z)) | AB
= (v02(#)(x2`|Z)) | AB + (u02(#)(y2`|Z)) | AB by CFUNCT_1:52
.= (v02| AB)(#)((x2`|Z)| AB) + (u02(#)(y2`|Z)) | AB
by A226,A227,CFUNCT_1:53
.= (v02| AB)(#)((x2`|Z)| AB) + (u02| AB)(#)((y2`|Z)| AB)
by A226,A227,CFUNCT_1:53;
hence thesis by A7,A24,A111,A128,A225;
end;
integral( v01(#)(x1`|Z) + u01(#)(y1`|Z),a,b )
= integral( v01(#)(x1`|Z) + u01(#)(y1`|Z),AB) by INTEGRA5:19
.= integral( (v02(#)(x2`|Z) + u02(#)(y2`|Z)),AB) by A222
.= integral( v02(#)(x2`|Z) + u02(#)(y2`|Z),a,b) by INTEGRA5:19;
hence thesis by A2,A3,A221;
end;
suppose
A228: a=b; then
reconsider BA=[.b,a.] as non empty closed_interval Subset of REAL
by MEASURE5:14;
A229: integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,a,b )
= integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,BA) by A228,INTEGRA5:19;
A230: -integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,BA)
= integral( u01(#)(x1`|Z) - v01(#)(y1`|Z) ,a,b ) by INTEGRA5:20;
A231:integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,a,b )
= integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,BA) by A228,INTEGRA5:19;
A232: -integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,BA)
= integral( v01(#)(x1`|Z) + u01(#)(y1`|Z) ,a,b ) by INTEGRA5:20;
integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,a,b )
= integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,BA) by A228,INTEGRA5:19;
then A233: integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,a,b )
= -integral( u02(#)(x2`|Z) - v02(#)(y2`|Z) ,a,b ) by INTEGRA5:20;
integral( v02(#)(x2`|Z) + u02(#)(y2`|Z) ,a,b )
= integral( v02(#)(x2`|Z) + u02(#)(y2`|Z) ,AB) by INTEGRA5:19;
then integral( v02(#)(x2`|Z) + u02(#)(y2`|Z) ,a,b )
= -integral( v02(#)(x2`|Z) + u02(#)(y2`|Z) ,a,b ) by A228,INTEGRA5:20;
hence thesis by A2,A3,A229,A230,A231,A232,A233;
end;
end;
definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
assume
A1: rng C c= dom f;
func integral(f,C) -> Complex means :Def4:
ex a,b be Real,x,y be PartFunc of REAL,REAL, Z be Subset of REAL st
a <= b & [.a,b.]=dom C & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z is open & [.a,b.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous &
y`|Z is continuous & C = (x+<i>(#)y) | [.a,b.]
& it = integral(f,x,y,a,b,Z);
existence
proof
consider a,b be Real,x,y be PartFunc of REAL,REAL,
Z be Subset of REAL such that
A2: a <= b & [.a,b.] = dom C & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z is open & [.a,b.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous & y`|Z is continuous &
C = (x+<i>(#)y) | [.a,b.] by Def3;
reconsider a,b as Real;
take integral(f,x,y,a,b,Z);
thus thesis by A2;
end;
uniqueness
proof
let s1,s2 be Complex;
assume
A3: ex a,b be Real,x,y be PartFunc of REAL,REAL,
Z be Subset of REAL st a <= b & [.a,b.]=dom C &
[.a,b.] c= dom x & [.a,b.] c= dom y & Z is open &
[.a,b.] c= Z & x is_differentiable_on Z & y is_differentiable_on Z &
x`|Z is continuous & y`|Z is continuous & C = (x+<i>(#)y) | [.a,b.] &
s1 = integral(f,x,y,a,b,Z);
assume
A4: ex a,b be Real,x,y be PartFunc of REAL,REAL,
Z be Subset of REAL st a <= b & [.a,b.]=dom C &
[.a,b.] c= dom x & [.a,b.] c= dom y & Z is open & [.a,b.] c= Z &
x is_differentiable_on Z & y is_differentiable_on Z &
x`|Z is continuous & y`|Z is continuous &
C = (x+<i>(#)y) | [.a,b.] &
s2 = integral(f,x,y,a,b,Z);
consider a1,b1 be Real,x1,y1 be PartFunc of REAL,REAL,
Z1 be Subset of REAL such that
A5: a1 <= b1 & [.a1,b1.]=dom C & [.a1,b1.] c= dom x1 & [.a1,b1.] c= dom y1 &
Z1 is open & [.a1,b1.] c= Z1 & x1 is_differentiable_on Z1 &
y1 is_differentiable_on Z1 & x1`|Z1 is continuous &
y1`|Z1 is continuous & C = (x1+<i>(#)y1) | [.a1,b1.] &
s1 = integral(f,x1,y1,a1,b1,Z1) by A3;
consider a2,b2 be Real,x2,y2 be PartFunc of REAL,REAL,
Z2 be Subset of REAL such that
A6: a2 <= b2 & [.a2,b2.] = dom C & [.a2,b2.] c= dom x2 & [.a2,b2.] c= dom y2 &
Z2 is open & [.a2,b2.] c= Z2 &
x2 is_differentiable_on Z2 & y2 is_differentiable_on Z2 &
x2`|Z2 is continuous & y2`|Z2 is continuous &
C = (x2+<i>(#)y2) | [.a2,b2.] &
s2 = integral(f,x2,y2,a2,b2,Z2) by A4;
dom C is non empty closed_interval Subset of REAL by A5,MEASURE5:14;
then
A7: a1 = a2 & b1 = b2 by A6,A5,INTEGRA1:5;
reconsider Z3 = Z1 /\ Z2 as Subset of REAL;
reconsider ZZ1=Z1, ZZ2= Z2 as Subset of R^1 by TOPMETR:17;
ZZ1 is open & ZZ2 is open by A5,A6,BORSUK_5:39;then
ZZ1 /\ ZZ2 is open by TOPS_1:11; then
A8: Z3 is open by BORSUK_5:39;
A9: x1| [.a1,b1.] = x2| [.a2,b2.]
proof
for x0 be set st x0 in [.a1,b1.] holds x1.x0 = x2.x0
proof
let x0 be set such that
A10: x0 in [.a1,b1.];
A11: dom(<i>(#)y1) = dom y1 by VALUED_1:def 5;
dom(x1+<i>(#)y1) = dom x1 /\ dom(<i>(#)y1) by VALUED_1:def 1;then
A12: [.a1,b1.] c= dom(x1+<i>(#)y1) by A5,A11,XBOOLE_1:19;
A13: ((x1+<i>(#)y1) | [.a1,b1.]).x0 = (x1+<i>(#)y1).x0 by A10,FUNCT_1:49
.= x1.x0 + (<i>(#)y1).x0 by A10,A12,VALUED_1:def 1
.= x1.x0 + <i>*y1.x0 by VALUED_1:6;
A14: dom(<i>(#)y2) = dom y2 by VALUED_1:def 5;
dom(x2+<i>(#)y2) = dom x2 /\ dom(<i>(#)y2) by VALUED_1:def 1;
then A15: [.a2,b2.] c= dom(x2+<i>(#)y2) by A6,A14,XBOOLE_1:19;
((x2+<i>(#)y2) | [.a2,b2.]).x0
= (x2+<i>(#)y2).x0 by A6,A5,A10,FUNCT_1:49
.= x2.x0 + (<i>(#)y2).x0 by A6,A5,A10,A15,VALUED_1:def 1
.= x2.x0 + <i>*y2.x0 by VALUED_1:6;
hence thesis by A6,A5,A13,COMPLEX1:77;
end;
hence thesis by A5,A6,FUNCT_1:95;
end;
A16: y1| [.a1,b1.] = y2| [.a2,b2.]
proof
for x0 be set st x0 in [.a1,b1.] holds y1.x0 = y2.x0
proof
let x0 be set such that
A17: x0 in [.a1,b1.];
A18: dom(<i>(#)y1) = dom y1 by VALUED_1:def 5;
dom(x1+<i>(#)y1) = dom x1 /\ dom(<i>(#)y1) by VALUED_1:def 1;then
A19: [.a1,b1.] c= dom(x1+<i>(#)y1) by A5,A18,XBOOLE_1:19;
A20: ((x1+<i>(#)y1) | [.a1,b1.]).x0 = (x1+<i>(#)y1).x0 by A17,FUNCT_1:49
.= x1.x0 + (<i>(#)y1).x0 by A17,A19,VALUED_1:def 1
.= x1.x0 + <i>*y1.x0 by VALUED_1:6;
A21: dom(<i>(#)y2) = dom y2 by VALUED_1:def 5;
dom(x2+<i>(#)y2) = dom x2 /\ dom(<i>(#)y2) by VALUED_1:def 1;
then A22: [.a2,b2.] c= dom(x2+<i>(#)y2) by A6,A21,XBOOLE_1:19;
((x2+<i>(#)y2) | [.a2,b2.]).x0
= (x2+<i>(#)y2).x0 by A5,A6,A17,FUNCT_1:49
.= x2.x0 + (<i>(#)y2).x0 by A5,A6,A17,A22,VALUED_1:def 1
.= x2.x0 + <i>*y2.x0 by VALUED_1:6;
hence thesis by A6,A5,A20,COMPLEX1:77;
end;
hence thesis by A5,A6,FUNCT_1:95;
end;
A23: [.a1,b1.] c= Z3 by A5,A6,XBOOLE_1:19;
A24: x1 is_differentiable_on Z3 &
y1 is_differentiable_on Z3 by A5,A8,FDIFF_1:26,XBOOLE_1:17;
A25: x2 is_differentiable_on Z3 &
y2 is_differentiable_on Z3 by A6,A8,FDIFF_1:26,XBOOLE_1:17;
thus s1 = integral(f,x1,y1,a1,b1,Z3) by A1,A5,A8,A23,Lm1,XBOOLE_1:17
.= integral(f,x2,y2,a2,b2,Z3)
by A1,A5,A6,A7,A8,A9,A16,A24,A25,Lm2,XBOOLE_1:19
.= s2 by A1,A6,A5,A8,A23,Lm1,XBOOLE_1:17;
end;
end;
definition
let f be PartFunc of COMPLEX,COMPLEX;
let C be C1-curve;
pred f is_integrable_on C means
for a,b be Real, x,y be PartFunc of REAL,REAL, Z be Subset of REAL,
u0,v0 be PartFunc of REAL,REAL st
(a <= b & [.a,b.]=dom C & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z is open & [.a,b.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous & y`|Z is continuous &
C = (x+<i>(#)y) | [.a,b.] ) holds
(u0(#)(x`|Z) - v0(#)(y`|Z)) is_integrable_on [' a,b '] &
(v0(#)(x`|Z) + u0(#)(y`|Z)) is_integrable_on [' a,b '];
end;
definition
let f be PartFunc of COMPLEX, COMPLEX;
let C be C1-curve;
pred f is_bounded_on C means
for a,b be Real, x,y be PartFunc of REAL,REAL, Z be Subset of REAL,
u0, v0 be PartFunc of REAL,REAL st
(a <= b & [.a,b.]=dom C & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z is open & [.a,b.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous & y`|Z is continuous &
C = (x+<i>(#)y) | [.a,b.] ) holds
(u0(#)(x`|Z) - v0(#)(y`|Z))|[' a,b '] is bounded &
(v0(#)(x`|Z) + u0(#)(y`|Z))|[' a,b '] is bounded;
end;
begin :: Linearity of Complex Intergal
theorem
for f,g be PartFunc of COMPLEX,COMPLEX, C be C1-curve
st rng C c= dom f & rng C c= dom g &
f is_integrable_on C & g is_integrable_on C &
f is_bounded_on C & g is_bounded_on C
holds
integral(f+g,C) = integral(f,C) + integral(g,C)
proof
let f,g be PartFunc of COMPLEX,COMPLEX,
C be C1-curve such that
A1: rng C c= dom f & rng C c= dom g & f is_integrable_on C &
g is_integrable_on C &
f is_bounded_on C & g is_bounded_on C;
consider a,b be Real,x,y be PartFunc of REAL,REAL,
Z be Subset of REAL such that
A2: a <= b & [.a,b.]=dom C & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z is open & [.a,b.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous &
y`|Z is continuous & C = (x+<i>(#)y) | [.a,b.] by Def3;
reconsider a,b as Real;
consider uf0,vf0 be PartFunc of REAL,REAL such that
A3: uf0=(Re f)* (R2-to-C) *<:x,y:> & vf0=(Im f)* (R2-to-C) *<:x,y:> &
integral(f,x,y,a,b,Z)
= integral( uf0(#)(x`|Z) - vf0(#)(y`|Z) ,a,b )
+ integral( vf0(#)(x`|Z) + uf0(#)(y`|Z) ,a,b )*<i> by Def2;
consider ug0,vg0 be PartFunc of REAL,REAL such that
A4: ug0=(Re g)* (R2-to-C) *<:x,y:> & vg0=(Im g)* (R2-to-C) *<:x,y:> &
integral(g,x,y,a,b,Z)
= integral( ug0(#)(x`|Z) - vg0(#)(y`|Z) ,a,b )
+ integral( vg0(#)(x`|Z) + ug0(#)(y`|Z) ,a,b )*<i> by Def2;
A5: integral(f,C) = integral(f,x,y,a,b,Z) &
integral(g,C) = integral(g,x,y,a,b,Z) by A1,A2,Def4;
A6: dom (f+g) = dom f /\ dom g by VALUED_1:def 1;
A7: rng C c= dom f /\ dom g by A1,XBOOLE_1:19;
consider u0,v0 be PartFunc of REAL,REAL such that
A8: u0=(Re(f+g))* (R2-to-C) *<:x,y:> & v0=(Im(f+g))* (R2-to-C) *<:x,y:> &
integral(f+g,x,y,a,b,Z)
= integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i> by Def2;
A9: u0(#)(x`|Z) = uf0(#)(x`|Z) + ug0(#)(x`|Z)
proof
A10: dom (uf0(#)(x`|Z) + ug0(#)(x`|Z))
= dom (uf0(#)(x`|Z)) /\ dom (ug0(#)(x`|Z)) by VALUED_1:def 1
.= (dom uf0 /\ dom (x`|Z)) /\ dom (ug0(#)(x`|Z)) by VALUED_1:def 4
.= (dom uf0 /\ dom (x`|Z)) /\ (dom ug0 /\ dom (x`|Z))
by VALUED_1:def 4
.= dom uf0 /\ (dom (x`|Z) /\ (dom ug0 /\ dom (x`|Z))) by XBOOLE_1:16
.= dom uf0 /\ ((dom (x`|Z) /\ dom (x`|Z)) /\ dom ug0) by XBOOLE_1:16
.= (dom uf0 /\ dom ug0) /\ dom (x`|Z) by XBOOLE_1:16;
A11: dom (u0(#)(x`|Z)) = dom u0 /\ dom (x`|Z) by VALUED_1:def 4;
A12: dom u0 = dom uf0 /\ dom ug0
proof
A13: for x0 be object st x0 in dom u0 holds x0 in dom uf0 /\ dom ug0
proof
let x0 be object such that
A14: x0 in dom u0;
A15: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re(f+g))*(R2-to-C)) by A14,A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A16: R2 in dom (R2-to-C) &
(R2-to-C).R2 in dom (Re(f+g)) by A15,FUNCT_1:11;then
(R2-to-C).R2 in dom (Re f + Re g) by MESFUN6C:5;then
(R2-to-C).R2 in (dom Re f /\ dom Re g) by VALUED_1:def 1;
then
(R2-to-C).R2 in dom Re f & (R2-to-C).R2 in dom Re g
by XBOOLE_0:def 4;then
R2 in dom ((Re f)*(R2-to-C)) &
R2 in dom ((Re g)*(R2-to-C)) by A16,FUNCT_1:11;then
x0 in dom uf0 & x0 in dom ug0 by A3,A4,A15,FUNCT_1:11;
hence thesis by XBOOLE_0:def 4;
end;
for x0 be object st x0 in dom uf0 /\ dom ug0 holds x0 in dom u0
proof
let x0 be object such that
A17: x0 in dom uf0 /\ dom ug0;
A18: x0 in dom uf0 & x0 in dom ug0 by A17,XBOOLE_0:def 4;
then A19: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re f)*(R2-to-C)) by A3,FUNCT_1:11;
A20: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re g)*(R2-to-C)) by A18,A4,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A21: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Re f) by A19,FUNCT_1:11;
R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Re g) by A20,FUNCT_1:11;then
(R2-to-C).R2 in dom (Re f) /\ dom (Re g) by A21,XBOOLE_0:def 4;
then
(R2-to-C).R2 in dom (Re f + Re g) by VALUED_1:def 1;then
(R2-to-C).R2 in dom (Re (f + g)) by MESFUN6C:5;then
R2 in dom ((Re (f + g))*(R2-to-C)) by A21,FUNCT_1:11;
hence thesis by A8,A19,FUNCT_1:11;
end;
hence thesis by A13,TARSKI:2;
end;
for x0 be object st x0 in dom (u0(#)(x`|Z))
holds (u0(#)(x`|Z)).x0 = (uf0(#)(x`|Z) + ug0(#)(x`|Z)).x0
proof
let x0 be object such that
A22: x0 in dom (u0(#)(x`|Z));
x0 in dom u0 /\ dom (x`|Z) by A22,VALUED_1:def 4;then
A23: x0 in dom u0 & x0 in dom (x`|Z) by XBOOLE_0:def 4;
then A24: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (f+g))*(R2-to-C))
by A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A25: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Re (f+g)) by A24,FUNCT_1:11;
set c0 = (R2-to-C).R2;
A26: u0.x0 = ((Re (f+g))*(R2-to-C)).R2 by A8,A23,FUNCT_1:12
.= (Re (f+g)).c0 by A24,FUNCT_1:12
.= (Re f + Re g).c0 by MESFUN6C:5;
A27: c0 in dom (Re f + Re g) by A25,MESFUN6C:5;
A28: x0 in dom uf0 & x0 in dom ug0 by A12,A23,XBOOLE_0:def 4;
then
A29: x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C)) by A3,FUNCT_1:11;
A30: uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A28,FUNCT_1:12
.= (Re f).c0 by A29,FUNCT_1:12;
A31: x0 in dom <:x,y:> & R2 in dom ((Re g)*(R2-to-C)) by A4,A28,FUNCT_1:11;
A32: ug0.x0 = ((Re g)*(R2-to-C)).R2 by A4,A28,FUNCT_1:12
.= (Re g).c0 by A31,FUNCT_1:12;
x0 in dom (uf0(#)(x`|Z)) /\ dom (ug0(#)(x`|Z))
by A10,A11,A12,A22,VALUED_1:def 1;
then
A33: x0 in dom (uf0(#)(x`|Z)) & x0 in dom (ug0(#)(x`|Z))
by XBOOLE_0:def 4;then
A34: (uf0(#)(x`|Z)).x0 = (Re f).c0*((x`|Z).x0) by A30,VALUED_1:def 4;
A35: (ug0(#)(x`|Z)).x0 = (Re g).c0*(x`|Z).x0 by A32,A33,VALUED_1:def 4;
(u0(#)(x`|Z)).x0 = (u0.x0)*((x`|Z).x0) by A22,VALUED_1:def 4
.= ((Re f).c0 + (Re g).c0)*((x`|Z).x0) by A26,A27,VALUED_1:def 1
.= (uf0(#)(x`|Z)).x0 + (ug0(#)(x`|Z)).x0 by A35,A34
.= (uf0(#)(x`|Z) + ug0(#)(x`|Z)).x0 by A10,A11,A12,A22,VALUED_1:def 1;
hence thesis;
end;
hence thesis by A10,A11,A12,FUNCT_1:2;
end;
A36: v0(#)(x`|Z) = vf0(#)(x`|Z) + vg0(#)(x`|Z)
proof
A37: dom (vf0(#)(x`|Z) + vg0(#)(x`|Z))
= dom (vf0(#)(x`|Z)) /\ dom (vg0(#)(x`|Z)) by VALUED_1:def 1
.= (dom vf0 /\ dom (x`|Z)) /\ dom (vg0(#)(x`|Z)) by VALUED_1:def 4
.= (dom vf0 /\ dom (x`|Z)) /\ (dom vg0 /\ dom (x`|Z)) by VALUED_1:def 4
.= dom vf0 /\ (dom (x`|Z) /\ (dom vg0 /\ dom (x`|Z))) by XBOOLE_1:16
.= dom vf0 /\ ((dom (x`|Z) /\ dom (x`|Z)) /\ dom vg0) by XBOOLE_1:16
.= (dom vf0 /\ dom vg0) /\ dom (x`|Z) by XBOOLE_1:16;
A38: dom (v0(#)(x`|Z)) = dom v0 /\ dom (x`|Z) by VALUED_1:def 4;
A39: dom v0 = dom vf0 /\ dom vg0
proof
A40: for x0 be object st x0 in dom v0 holds x0 in dom vf0 /\ dom vg0
proof
let x0 be object such that
A41: x0 in dom v0;
A42: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im(f+g))*(R2-to-C)) by A41,A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A43: R2 in dom (R2-to-C) &
(R2-to-C).R2 in dom (Im(f+g)) by A42,FUNCT_1:11;then
(R2-to-C).R2 in dom (Im f + Im g) by MESFUN6C:5;then
(R2-to-C).R2 in (dom Im f /\ dom Im g) by VALUED_1:def 1;
then
(R2-to-C).R2 in dom Im f & (R2-to-C).R2 in dom Im g
by XBOOLE_0:def 4;then
R2 in dom ((Im f)*(R2-to-C)) &
R2 in dom ((Im g)*(R2-to-C)) by A43,FUNCT_1:11;then
x0 in dom vf0 & x0 in dom vg0 by A3,A4,A42,FUNCT_1:11;
hence thesis by XBOOLE_0:def 4;
end;
for x0 be object st x0 in dom vf0 /\ dom vg0 holds x0 in dom v0
proof
let x0 be object such that
A44: x0 in dom vf0 /\ dom vg0;
A45: x0 in dom vf0 & x0 in dom vg0 by A44,XBOOLE_0:def 4;
then A46: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im f)*(R2-to-C)) by A3,FUNCT_1:11;
A47: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im g)*(R2-to-C)) by A45,A4,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A48: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Im f) by A46,FUNCT_1:11;
R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Im g) by A47,FUNCT_1:11;then
(R2-to-C).R2 in dom (Im f) /\ dom (Im g) by A48,XBOOLE_0:def 4;
then
(R2-to-C).R2 in dom (Im f + Im g) by VALUED_1:def 1;then
(R2-to-C).R2 in dom (Im (f + g)) by MESFUN6C:5;then
R2 in dom ((Im (f + g))*(R2-to-C)) by A48,FUNCT_1:11;
hence thesis by A8,A46,FUNCT_1:11;
end;
hence thesis by A40,TARSKI:2;
end;
for x0 be object st x0 in dom (v0(#)(x`|Z))
holds (v0(#)(x`|Z)).x0 = (vf0(#)(x`|Z) + vg0(#)(x`|Z)).x0
proof
let x0 be object such that
A49: x0 in dom (v0(#)(x`|Z));
x0 in dom v0 /\ dom (x`|Z) by A49,VALUED_1:def 4;then
A50: x0 in dom v0 & x0 in dom (x`|Z) by XBOOLE_0:def 4;
then A51: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (f+g))*(R2-to-C))
by A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A52: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Im (f+g)) by A51,FUNCT_1:11;
set c0 = (R2-to-C).R2;
A53: v0.x0 = ((Im (f+g))*(R2-to-C)).R2 by A8,A50,FUNCT_1:12
.= (Im (f+g)).c0 by A51,FUNCT_1:12
.= (Im f + Im g).c0 by MESFUN6C:5;
A54: c0 in dom (Im f + Im g) by A52,MESFUN6C:5;
A55: x0 in dom vf0 & x0 in dom vg0 by A39,A50,XBOOLE_0:def 4;
then
A56: x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C)) by A3,FUNCT_1:11;
A57: vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A55,FUNCT_1:12
.= (Im f).c0 by A56,FUNCT_1:12;
A58: x0 in dom <:x,y:> & R2 in dom ((Im g)*(R2-to-C)) by A4,A55,FUNCT_1:11;
A59: vg0.x0 = ((Im g)*(R2-to-C)).R2 by A4,A55,FUNCT_1:12
.= (Im g).c0 by A58,FUNCT_1:12;
x0 in dom (vf0(#)(x`|Z)) /\ dom (vg0(#)(x`|Z))
by A37,A38,A39,A49,VALUED_1:def 1;
then
A60: x0 in dom (vf0(#)(x`|Z)) & x0 in dom (vg0(#)(x`|Z))
by XBOOLE_0:def 4;then
A61: (vf0(#)(x`|Z)).x0 = (Im f).c0*((x`|Z).x0) by A57,VALUED_1:def 4;
A62: (vg0(#)(x`|Z)).x0 = (Im g).c0*(x`|Z).x0 by A59,A60,VALUED_1:def 4;
(v0(#)(x`|Z)).x0 = (v0.x0)*((x`|Z).x0) by A49,VALUED_1:def 4
.= ((Im f).c0 + (Im g).c0)*((x`|Z).x0)
by A53,A54,VALUED_1:def 1
.= (vf0(#)(x`|Z)).x0 + (vg0(#)(x`|Z)).x0 by A62,A61
.= (vf0(#)(x`|Z) + vg0(#)(x`|Z)).x0 by A37,A38,A39,A49,VALUED_1:def 1;
hence thesis;
end;
hence thesis by A37,A38,A39,FUNCT_1:2;
end;
A63: u0(#)(y`|Z) = uf0(#)(y`|Z) + ug0(#)(y`|Z)
proof
A64: dom (uf0(#)(y`|Z) + ug0(#)(y`|Z))
= dom (uf0(#)(y`|Z)) /\ dom (ug0(#)(y`|Z)) by VALUED_1:def 1
.= (dom uf0 /\ dom (y`|Z)) /\ dom (ug0(#)(y`|Z)) by VALUED_1:def 4
.= (dom uf0 /\ dom (y`|Z)) /\ (dom ug0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom uf0 /\ (dom (y`|Z) /\ (dom ug0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom uf0 /\ ((dom (y`|Z) /\ dom (y`|Z)) /\ dom ug0) by XBOOLE_1:16
.= (dom uf0 /\ dom ug0) /\ dom (y`|Z) by XBOOLE_1:16;
A65: dom (u0(#)(y`|Z)) = dom u0 /\ dom (y`|Z) by VALUED_1:def 4;
A66: dom u0 = dom uf0 /\ dom ug0
proof
A67: for x0 be object st x0 in dom u0 holds x0 in dom uf0 /\ dom ug0
proof
let x0 be object such that
A68: x0 in dom u0;
A69: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re(f+g))*(R2-to-C)) by A68,A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A70: R2 in dom (R2-to-C) &
(R2-to-C).R2 in dom (Re(f+g)) by A69,FUNCT_1:11;then
(R2-to-C).R2 in dom (Re f + Re g) by MESFUN6C:5;then
(R2-to-C).R2 in (dom Re f /\ dom Re g) by VALUED_1:def 1;
then
(R2-to-C).R2 in dom Re f & (R2-to-C).R2 in dom Re g
by XBOOLE_0:def 4;then
R2 in dom ((Re f)*(R2-to-C)) &
R2 in dom ((Re g)*(R2-to-C)) by A70,FUNCT_1:11;then
x0 in dom uf0 & x0 in dom ug0 by A3,A4,A69,FUNCT_1:11;
hence thesis by XBOOLE_0:def 4;
end;
for x0 be object st x0 in dom uf0 /\ dom ug0 holds x0 in dom u0
proof
let x0 be object such that
A71: x0 in dom uf0 /\ dom ug0;
A72: x0 in dom uf0 & x0 in dom ug0 by A71,XBOOLE_0:def 4;
then A73: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re f)*(R2-to-C)) by A3,FUNCT_1:11;
A74: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re g)*(R2-to-C)) by A72,A4,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A75: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Re f) by A73,FUNCT_1:11;
R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Re g) by A74,FUNCT_1:11;then
(R2-to-C).R2 in dom (Re f) /\ dom (Re g) by A75,XBOOLE_0:def 4;
then
(R2-to-C).R2 in dom (Re f + Re g) by VALUED_1:def 1;then
(R2-to-C).R2 in dom (Re (f + g)) by MESFUN6C:5;then
R2 in dom ((Re (f + g))*(R2-to-C)) by A75,FUNCT_1:11;
hence thesis by A8,A73,FUNCT_1:11;
end;
hence thesis by A67,TARSKI:2;
end;
for x0 be object st x0 in dom (u0(#)(y`|Z))
holds (u0(#)(y`|Z)).x0 = (uf0(#)(y`|Z) + ug0(#)(y`|Z)).x0
proof
let x0 be object such that
A76: x0 in dom (u0(#)(y`|Z));
x0 in dom u0 /\ dom (y`|Z) by A76,VALUED_1:def 4;then
A77: x0 in dom u0 & x0 in dom (y`|Z) by XBOOLE_0:def 4;
then A78: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (f+g))*(R2-to-C))
by A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A79: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Re (f+g)) by A78,FUNCT_1:11;
set c0 = (R2-to-C).R2;
A80: u0.x0 = ((Re (f+g))*(R2-to-C)).R2 by A8,A77,FUNCT_1:12
.= (Re (f+g)).c0 by A78,FUNCT_1:12
.= (Re f + Re g).c0 by MESFUN6C:5;
A81: c0 in dom (Re f + Re g) by A79,MESFUN6C:5;
A82: x0 in dom uf0 & x0 in dom ug0 by A66,A77,XBOOLE_0:def 4;
then
A83: x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C)) by A3,FUNCT_1:11;
A84: uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A82,FUNCT_1:12
.= (Re f).c0 by A83,FUNCT_1:12;
A85: x0 in dom <:x,y:> & R2 in dom ((Re g)*(R2-to-C)) by A4,A82,FUNCT_1:11;
A86: ug0.x0 = ((Re g)*(R2-to-C)).R2 by A4,A82,FUNCT_1:12
.= (Re g).c0 by A85,FUNCT_1:12;
x0 in dom (uf0(#)(y`|Z)) /\ dom (ug0(#)(y`|Z))
by A64,A65,A66,A76,VALUED_1:def 1; then
A87: x0 in dom (uf0(#)(y`|Z)) & x0 in dom (ug0(#)(y`|Z))
by XBOOLE_0:def 4;then
A88: (uf0(#)(y`|Z)).x0 = (Re f).c0*((y`|Z).x0) by A84,VALUED_1:def 4;
A89: (ug0(#)(y`|Z)).x0 = (Re g).c0*(y`|Z).x0 by A86,A87,VALUED_1:def 4;
(u0(#)(y`|Z)).x0 = (u0.x0)*((y`|Z).x0) by A76,VALUED_1:def 4
.= ((Re f).c0 + (Re g).c0)*((y`|Z).x0) by A80,A81,VALUED_1:def 1
.= (uf0(#)(y`|Z)).x0 + (ug0(#)(y`|Z)).x0 by A89,A88
.= (uf0(#)(y`|Z) + ug0(#)(y`|Z)).x0
by A64,A65,A66,A76,VALUED_1:def 1;
hence thesis;
end;
hence thesis by A64,A65,A66,FUNCT_1:2;
end;
A90: v0(#)(y`|Z) = vf0(#)(y`|Z) + vg0(#)(y`|Z)
proof
A91: dom (vf0(#)(y`|Z) + vg0(#)(y`|Z))
= dom (vf0(#)(y`|Z)) /\ dom (vg0(#)(y`|Z)) by VALUED_1:def 1
.= (dom vf0 /\ dom (y`|Z)) /\ dom (vg0(#)(y`|Z)) by VALUED_1:def 4
.= (dom vf0 /\ dom (y`|Z)) /\ (dom vg0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom vf0 /\ (dom (y`|Z) /\ (dom vg0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom vf0 /\ ((dom (y`|Z) /\ dom (y`|Z)) /\ dom vg0) by XBOOLE_1:16
.= (dom vf0 /\ dom vg0) /\ dom (y`|Z) by XBOOLE_1:16;
A92: dom (v0(#)(y`|Z)) = dom v0 /\ dom (y`|Z) by VALUED_1:def 4;
A93: dom v0 = dom vf0 /\ dom vg0
proof
A94: for x0 be object st x0 in dom v0 holds x0 in dom vf0 /\ dom vg0
proof
let x0 be object such that
A95: x0 in dom v0;
A96: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im(f+g))*(R2-to-C)) by A8,A95,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A97: R2 in dom (R2-to-C) &
(R2-to-C).R2 in dom (Im(f+g)) by A96,FUNCT_1:11;then
(R2-to-C).R2 in dom (Im f + Im g) by MESFUN6C:5;then
(R2-to-C).R2 in (dom Im f /\ dom Im g) by VALUED_1:def 1;
then
(R2-to-C).R2 in dom Im f & (R2-to-C).R2 in dom Im g
by XBOOLE_0:def 4;then
R2 in dom ((Im f)*(R2-to-C)) &
R2 in dom ((Im g)*(R2-to-C)) by A97,FUNCT_1:11;then
x0 in dom vf0 & x0 in dom vg0 by A3,A4,A96,FUNCT_1:11;
hence thesis by XBOOLE_0:def 4;
end;
for x0 be object st x0 in dom vf0 /\ dom vg0 holds x0 in dom v0
proof
let x0 be object such that
A98: x0 in dom vf0 /\ dom vg0;
A99: x0 in dom vf0 & x0 in dom vg0 by A98,XBOOLE_0:def 4;
then A100: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im f)*(R2-to-C)) by A3,FUNCT_1:11;
A101: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im g)*(R2-to-C)) by A99,A4,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A102: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Im f) by A100,FUNCT_1:11;
R2 in dom (R2-to-C) &
(R2-to-C).R2 in dom (Im g) by A101,FUNCT_1:11;then
(R2-to-C).R2 in dom (Im f) /\ dom (Im g) by A102,XBOOLE_0:def 4;
then
(R2-to-C).R2 in dom (Im f + Im g) by VALUED_1:def 1;then
(R2-to-C).R2 in dom (Im (f + g)) by MESFUN6C:5;then
R2 in dom ((Im (f + g))*(R2-to-C)) by A102,FUNCT_1:11;
hence thesis by A8,A100,FUNCT_1:11;
end;
hence thesis by A94,TARSKI:2;
end;
for x0 be object st x0 in dom (v0(#)(y`|Z))
holds (v0(#)(y`|Z)).x0 = (vf0(#)(y`|Z) + vg0(#)(y`|Z)).x0
proof
let x0 be object such that
A103: x0 in dom (v0(#)(y`|Z));
x0 in dom v0 /\ dom (y`|Z) by A103,VALUED_1:def 4;then
A104: x0 in dom v0 & x0 in dom (y`|Z) by XBOOLE_0:def 4;
then A105: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (f+g))*(R2-to-C))
by A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A106: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Im (f+g)) by A105,FUNCT_1:11;
set c0 = (R2-to-C).R2;
A107: v0.x0 = ((Im (f+g))*(R2-to-C)).R2 by A8,A104,FUNCT_1:12
.= (Im (f+g)).c0 by A105,FUNCT_1:12
.= (Im f + Im g).c0 by MESFUN6C:5;
A108: c0 in dom (Im f + Im g) by A106,MESFUN6C:5;
A109: x0 in dom vf0 & x0 in dom vg0 by A93,A104,XBOOLE_0:def 4;
then
A110: x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C)) by A3,FUNCT_1:11;
A111: vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A109,FUNCT_1:12
.= (Im f).c0 by A110,FUNCT_1:12;
A112: x0 in dom <:x,y:> & R2 in dom ((Im g)*(R2-to-C)) by A4,A109,FUNCT_1:11;
A113: vg0.x0 = ((Im g)*(R2-to-C)).R2 by A4,A109,FUNCT_1:12
.= (Im g).c0 by A112,FUNCT_1:12;
x0 in dom (vf0(#)(y`|Z)) /\ dom (vg0(#)(y`|Z))
by A91,A92,A93,A103,VALUED_1:def 1;
then
A114: x0 in dom (vf0(#)(y`|Z)) & x0 in dom (vg0(#)(y`|Z))
by XBOOLE_0:def 4;then
A115: (vf0(#)(y`|Z)).x0 = (Im f).c0*((y`|Z).x0) by A111,VALUED_1:def 4;
A116: (vg0(#)(y`|Z)).x0 = (Im g).c0*(y`|Z).x0 by A113,A114,VALUED_1:def 4;
(v0(#)(y`|Z)).x0 = (v0.x0)*((y`|Z).x0) by A103,VALUED_1:def 4
.= ((Im f).c0 + (Im g).c0)*((y`|Z).x0) by A107,A108,VALUED_1:def 1
.= (vf0(#)(y`|Z)).x0 + (vg0(#)(y`|Z)).x0 by A116,A115
.= (vf0(#)(y`|Z) + vg0(#)(y`|Z)).x0
by A91,A92,A93,A103,VALUED_1:def 1;
hence thesis;
end;
hence thesis by A91,A92,A93,FUNCT_1:2;
end;
A117: [.a,b.] c= dom uf0
proof
let x0 be object such that
A118: x0 in [.a,b.];
A119: C.x0 in rng C by A2,A118,FUNCT_1:3;
A120: x0 in dom x & x0 in dom y by A2,A118;
A121: x0 in dom x /\ dom y by A118,A2,XBOOLE_0:def 4;then
A122: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A121,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A123: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A120,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A2,A118,XBOOLE_0:def 4;
then
A124: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A125: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A126: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A118,A2,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A124,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A125,A126,Def1
.= (R2-to-C).R2 by A121,FUNCT_3:48;then
(R2-to-C).R2 in dom f by A1,A119;then
(R2-to-C).R2 in dom (Re f) by COMSEQ_3:def 3;then
R2 in dom ((Re f)* (R2-to-C)) by A123,FUNCT_1:11;
hence thesis by A3,A122,FUNCT_1:11;
end;
A127: [.a,b.] c= dom vf0
proof
let x0 be object such that
A128: x0 in [.a,b.];
A129: C.x0 in rng C by A2,A128,FUNCT_1:3;
A130: x0 in dom x & x0 in dom y by A2,A128;
A131: x0 in dom x /\ dom y by A2,A128,XBOOLE_0:def 4;then
A132: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A131,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A133: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A130,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A2,A128,XBOOLE_0:def 4;
then
A134: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A135: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A136: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A128,A2,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A134,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A135,A136,Def1
.= (R2-to-C).R2 by A131,FUNCT_3:48;then
(R2-to-C).R2 in dom f by A1,A129;then
(R2-to-C).R2 in dom (Im f) by COMSEQ_3:def 4;then
R2 in dom ((Im f)* (R2-to-C)) by A133,FUNCT_1:11;
hence thesis by A3,A132,FUNCT_1:11;
end;
A137: [.a,b.] c= dom ug0
proof
let x0 be object such that
A138: x0 in [.a,b.];
A139: C.x0 in rng C by A138,A2,FUNCT_1:3;
A140: x0 in dom x & x0 in dom y by A2,A138;
A141: x0 in dom x /\ dom y by A2,A138,XBOOLE_0:def 4;then
A142: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A141,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A143: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A140,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A2,A138,XBOOLE_0:def 4;
then
A144: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A145: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A146: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A138,A2,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A144,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A145,A146,Def1
.= (R2-to-C).R2 by A141,FUNCT_3:48;then
(R2-to-C).R2 in dom g by A1,A139;then
(R2-to-C).R2 in dom (Re g) by COMSEQ_3:def 3;then
R2 in dom ((Re g)* (R2-to-C)) by A143,FUNCT_1:11;
hence thesis by A4,A142,FUNCT_1:11;
end;
A147: [.a,b.] c= dom vg0
proof
let x0 be object such that
A148: x0 in [.a,b.];
A149: C.x0 in rng C by A2,A148,FUNCT_1:3;
A150: x0 in dom x & x0 in dom y by A2,A148;
A151: x0 in dom x /\ dom y by A148,A2,XBOOLE_0:def 4;then
A152: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A151,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A153: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A150,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A2,A148,XBOOLE_0:def 4;
then
A154: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A155: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A156: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A148,A2,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A154,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A155,A156,Def1
.= (R2-to-C).R2 by A151,FUNCT_3:48;then
(R2-to-C).R2 in dom g by A1,A149;then
(R2-to-C).R2 in dom (Im g) by COMSEQ_3:def 4;then
R2 in dom ((Im g)* (R2-to-C)) by A153,FUNCT_1:11;
hence thesis by A4,A152,FUNCT_1:11;
end;
A157: [' a,b '] c= dom (uf0(#)(x`|Z) - vf0(#)(y`|Z))
proof
A158: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 3;
A159: dom (uf0(#)(x`|Z) - vf0(#)(y`|Z))
= dom (uf0(#)(x`|Z)) /\ dom (vf0(#)(y`|Z)) by VALUED_1:12
.= (dom uf0 /\ dom (x`|Z)) /\ dom (vf0(#)(y`|Z)) by VALUED_1:def 4
.= (dom uf0 /\ dom (x`|Z)) /\ (dom vf0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom uf0 /\ ((dom (x`|Z)) /\ (dom vf0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom uf0 /\ ((Z) /\ ((dom (y`|Z)) /\ dom vf0)) by A2,FDIFF_1:def 7
.= dom uf0 /\ (Z /\ (Z /\ dom vf0)) by A2,FDIFF_1:def 7
.= dom uf0 /\ ((Z /\ Z) /\ dom vf0) by XBOOLE_1:16
.= (dom uf0 /\ dom vf0) /\ Z by XBOOLE_1:16;
[.a,b.] c= dom uf0 /\ dom vf0 by A117,A127,XBOOLE_1:19;
hence thesis by A2,A158,A159,XBOOLE_1:19;
end;
A160: [' a,b '] c= dom (ug0(#)(x`|Z) - vg0(#)(y`|Z))
proof
A161: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 3;
A162: dom (ug0(#)(x`|Z) - vg0(#)(y`|Z))
= dom (ug0(#)(x`|Z)) /\ dom (vg0(#)(y`|Z)) by VALUED_1:12
.= (dom ug0 /\ dom (x`|Z)) /\ dom (vg0(#)(y`|Z)) by VALUED_1:def 4
.= (dom ug0 /\ dom (x`|Z)) /\ (dom vg0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom ug0 /\ ((dom (x`|Z)) /\ (dom vg0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom ug0 /\ ((Z) /\ ((dom (y`|Z)) /\ dom vg0)) by A2,FDIFF_1:def 7
.= dom ug0 /\ (Z /\ (Z /\ dom vg0)) by A2,FDIFF_1:def 7
.= dom ug0 /\ ((Z /\ Z) /\ dom vg0) by XBOOLE_1:16
.= (dom ug0 /\ dom vg0) /\ Z by XBOOLE_1:16;
[.a,b.] c= dom ug0 /\ dom vg0 by A137,A147,XBOOLE_1:19;
hence thesis by A2,A161,A162,XBOOLE_1:19;
end;
A163: [' a,b '] c= dom (vf0(#)(x`|Z) + uf0(#)(y`|Z))
proof
A164: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 3;
A165: dom (vf0(#)(x`|Z) + uf0(#)(y`|Z))
= dom (vf0(#)(x`|Z)) /\ dom (uf0(#)(y`|Z)) by VALUED_1:def 1
.= (dom vf0 /\ dom (x`|Z)) /\ dom (uf0(#)(y`|Z)) by VALUED_1:def 4
.= (dom vf0 /\ dom (x`|Z)) /\ (dom uf0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom vf0 /\ ((dom (x`|Z)) /\ (dom uf0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom vf0 /\ ((Z) /\ ((dom (y`|Z)) /\ dom uf0)) by A2,FDIFF_1:def 7
.= dom vf0 /\ (Z /\ (Z /\ dom uf0)) by A2,FDIFF_1:def 7
.= dom vf0 /\ ((Z /\ Z) /\ dom uf0) by XBOOLE_1:16
.= (dom vf0 /\ dom uf0) /\ Z by XBOOLE_1:16;
[.a,b.] c= dom vf0 /\ dom uf0 by A117,A127,XBOOLE_1:19;
hence thesis by A2,A164,A165,XBOOLE_1:19;
end;
A166: [' a,b '] c= dom (vg0(#)(x`|Z) + ug0(#)(y`|Z))
proof
A167: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 3;
A168: dom (vg0(#)(x`|Z) + ug0(#)(y`|Z))
= dom (vg0(#)(x`|Z)) /\ dom (ug0(#)(y`|Z)) by VALUED_1:def 1
.= (dom vg0 /\ dom (x`|Z)) /\ dom (ug0(#)(y`|Z)) by VALUED_1:def 4
.= (dom vg0 /\ dom (x`|Z)) /\ (dom ug0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom vg0 /\ ((dom (x`|Z)) /\ (dom ug0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom vg0 /\ ((Z) /\ ((dom (y`|Z)) /\ dom ug0)) by A2,FDIFF_1:def 7
.= dom vg0 /\ (Z /\ (Z /\ dom ug0)) by A2,FDIFF_1:def 7
.= dom vg0 /\ ((Z /\ Z) /\ dom ug0) by XBOOLE_1:16
.= (dom vg0 /\ dom ug0) /\ Z by XBOOLE_1:16;
[.a,b.] c= dom ug0 /\ dom vg0 by A137,A147,XBOOLE_1:19;
hence thesis by A2,A167,A168,XBOOLE_1:19;
end;
reconsider a,b as Real;
A169: (uf0(#)(x`|Z) - vf0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2;
A170: (ug0(#)(x`|Z) - vg0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2;
A171: (vf0(#)(x`|Z) + uf0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2;
A172: (vg0(#)(x`|Z) + ug0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2;
A173: (uf0(#)(x`|Z) - vf0(#)(y`|Z))|[' a,b '] is bounded by A1,A2;
A174: (ug0(#)(x`|Z) - vg0(#)(y`|Z))|[' a,b '] is bounded by A1,A2;
A175: (vf0(#)(x`|Z) + uf0(#)(y`|Z))|[' a,b '] is bounded by A1,A2;
A176: (vg0(#)(x`|Z) + ug0(#)(y`|Z))|[' a,b '] is bounded by A1,A2;
integral(f+g,C)
= integral(uf0(#)(x`|Z)+ug0(#)(x`|Z)-(vf0(#)(y`|Z)+vg0(#)(y`|Z)),a,b )
+ integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+(uf0(#)(y`|Z)+ug0(#)(y`|Z)),a,b )*<i>
by A36,A63,A9,A90,A8,A2,A6,A7,Def4
.= integral(uf0(#)(x`|Z)+ug0(#)(x`|Z)-vf0(#)(y`|Z)-vg0(#)(y`|Z),a,b )
+ integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+(uf0(#)(y`|Z)+ug0(#)(y`|Z)),a,b )*<i>
by RFUNCT_1:20
.= integral(uf0(#)(x`|Z)+ug0(#)(x`|Z)-vf0(#)(y`|Z)-vg0(#)(y`|Z),a,b )
+ integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+uf0(#)(y`|Z)+ug0(#)(y`|Z),a,b )*<i>
by RFUNCT_1:8
.= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z)+ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
+ integral(vf0(#)(x`|Z)+vg0(#)(x`|Z)+uf0(#)(y`|Z)+ug0(#)(y`|Z),a,b )*<i>
by RFUNCT_1:8
.= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z) + ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
+ integral(vf0(#)(x`|Z)+uf0(#)(y`|Z) + vg0(#)(x`|Z)+ug0(#)(y`|Z),a,b )*<i>
by RFUNCT_1:8
.= integral((uf0(#)(x`|Z)-vf0(#)(y`|Z)) + (ug0(#)(x`|Z)-vg0(#)(y`|Z)),a,b )
+ integral(vf0(#)(x`|Z)+uf0(#)(y`|Z) + vg0(#)(x`|Z)+ug0(#)(y`|Z),a,b )*<i>
by RFUNCT_1:8
.= integral((uf0(#)(x`|Z)-vf0(#)(y`|Z))
+ (ug0(#)(x`|Z)-vg0(#)(y`|Z)),a,b )
+ integral((vf0(#)(x`|Z)+uf0(#)(y`|Z))
+ (vg0(#)(x`|Z)+ug0(#)(y`|Z)),a,b )*<i> by RFUNCT_1:8
.= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z),a,b )
+ integral(ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
+ integral((vf0(#)(x`|Z)+uf0(#)(y`|Z))
+ (vg0(#)(x`|Z)+ug0(#)(y`|Z)),a,b )*<i>
by A2,A157,A160,A169,A170,A173,A174,INTEGRA6:12
.= integral(uf0(#)(x`|Z)-vf0(#)(y`|Z),a,b )
+ integral(ug0(#)(x`|Z)-vg0(#)(y`|Z),a,b )
+ (integral(vf0(#)(x`|Z)+uf0(#)(y`|Z),a,b )
+ integral(vg0(#)(x`|Z)+ug0(#)(y`|Z),a,b ))*<i>
by A2,A163,A166,A171,A172,A175,A176,INTEGRA6:12
.= integral(f,C) + integral(g,C) by A4,A5,A3;
hence thesis;
end;
theorem
for f be PartFunc of COMPLEX,COMPLEX,
C be C1-curve st rng C c= dom f & f is_integrable_on C &
f is_bounded_on C holds
for r be Real holds
integral(r(#)f,C) = r*integral(f,C)
proof
let f be PartFunc of COMPLEX,COMPLEX,
C be C1-curve such that
A1: rng C c= dom f & f is_integrable_on C & f is_bounded_on C;
let r be Real;
consider a,b be Real,x,y be PartFunc of REAL,REAL,
Z be Subset of REAL such that
A2: a <= b & [.a,b.]=dom C & [.a,b.] c= dom x & [.a,b.] c= dom y &
Z is open & [.a,b.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous & y`|Z is continuous &
C = (x+<i>(#)y) | [.a,b.] by Def3;
reconsider a,b as Real;
consider uf0,vf0 be PartFunc of REAL,REAL such that
A3: uf0=(Re f)* (R2-to-C) *<:x,y:> & vf0=(Im f)* (R2-to-C) *<:x,y:> &
integral(f,x,y,a,b,Z)
= integral( uf0(#)(x`|Z) - vf0(#)(y`|Z) ,a,b )
+ integral( vf0(#)(x`|Z) + uf0(#)(y`|Z) ,a,b )*<i> by Def2;
A4: dom (r(#)f) = dom f by VALUED_1:def 5;
consider u0,v0 be PartFunc of REAL,REAL such that
A5: u0=(Re(r(#)f))* (R2-to-C) *<:x,y:> & v0=(Im(r(#)f))* (R2-to-C) *<:x,y:> &
integral(r(#)f,x,y,a,b,Z) = integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i> by Def2;
A6: dom u0 = dom uf0
proof
A7: for x0 be object st x0 in dom u0 holds x0 in dom uf0
proof
let x0 be object such that
A8: x0 in dom u0;
A9: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re(r(#)f))*(R2-to-C)) by A5,A8,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A10: R2 in dom (R2-to-C) &
(R2-to-C).R2 in dom (Re(r(#)f)) by A9,FUNCT_1:11;then
(R2-to-C).R2 in dom (r(#)Re f) by MESFUN6C:2;then
(R2-to-C).R2 in (dom Re f) by VALUED_1:def 5;then
R2 in dom ((Re f)*(R2-to-C)) by A10,FUNCT_1:11;
hence thesis by A3,A9,FUNCT_1:11;
end;
for x0 be object st x0 in dom uf0 holds x0 in dom u0
proof
let x0 be object such that
A11: x0 in dom uf0;
A12: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Re f)*(R2-to-C)) by A3,A11,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A13: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Re f) by A12,FUNCT_1:11;then
(R2-to-C).R2 in dom (r(#)Re f) by VALUED_1:def 5;then
(R2-to-C).R2 in dom (Re(r(#)f)) by MESFUN6C:2;then
R2 in dom ((Re (r(#)f))*(R2-to-C)) by A13,FUNCT_1:11;
hence thesis by A5,A12,FUNCT_1:11;
end;
hence thesis by A7,TARSKI:2;
end;
A14: dom v0 = dom vf0
proof
A15: for x0 be object st x0 in dom v0 holds x0 in dom vf0
proof
let x0 be object such that
A16: x0 in dom v0;
A17: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im(r(#)f))*(R2-to-C)) by A16,A5,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A18: R2 in dom (R2-to-C) &
(R2-to-C).R2 in dom (Im(r(#)f)) by A17,FUNCT_1:11;then
(R2-to-C).R2 in dom (r(#)Im f) by MESFUN6C:2;then
(R2-to-C).R2 in (dom Im f) by VALUED_1:def 5;then
R2 in dom ((Im f)*(R2-to-C)) by A18,FUNCT_1:11;
hence thesis by A3,A17,FUNCT_1:11;
end;
for x0 be object st x0 in dom vf0 holds x0 in dom v0
proof
let x0 be object such that
A19: x0 in dom vf0;
A20: x0 in dom <:x,y:> &
<:x,y:>.x0 in dom ((Im f)*(R2-to-C)) by A19,A3,FUNCT_1:11;
set R2 = <:x,y:>.x0;
A21: R2 in dom (R2-to-C) & (R2-to-C).R2 in dom (Im f) by A20,FUNCT_1:11;then
(R2-to-C).R2 in dom (r(#)Im f) by VALUED_1:def 5;then
(R2-to-C).R2 in dom (Im(r(#)f)) by MESFUN6C:2;then
R2 in dom ((Im (r(#)f))*(R2-to-C)) by A21,FUNCT_1:11;
hence thesis by A5,A20,FUNCT_1:11;
end;
hence thesis by A15,TARSKI:2;
end;
A22: u0(#)(x`|Z) = r(#)(uf0(#)(x`|Z))
proof
A23: dom (r(#)(uf0(#)(x`|Z))) = dom (uf0(#)(r(#)(x`|Z))) by RFUNCT_1:13
.= dom(uf0) /\ dom (r(#)(x`|Z)) by VALUED_1:def 4
.= dom uf0 /\ dom (x`|Z) by VALUED_1:def 5;
A24: dom (u0(#)(x`|Z)) = dom u0 /\ dom (x`|Z) by VALUED_1:def 4;
A25: dom (u0(#)(x`|Z)) = dom (r(#)(uf0(#)(x`|Z))) by A6,A23,VALUED_1:def 4;
for x0 be object st x0 in dom (u0(#)(x`|Z))
holds (u0(#)(x`|Z)).x0 = (r(#)(uf0(#)(x`|Z))).x0
proof
let x0 be object such that
A26: x0 in dom (u0(#)(x`|Z));
A27: x0 in dom u0 /\ dom (x`|Z) by A26,VALUED_1:def 4;then
A28: x0 in dom u0 & x0 in dom (x`|Z) by XBOOLE_0:def 4;
then A29: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (r(#)f))*(R2-to-C))
by A5,FUNCT_1:11;
set R2 = <:x,y:>.x0;
set c0 = (R2-to-C).R2;
A30: u0.x0 = ((Re (r(#)f))*(R2-to-C)).R2 by A5,A28,FUNCT_1:12
.= (Re (r(#)f)).c0 by A29,FUNCT_1:12
.= (r(#)Re f).c0 by MESFUN6C:2;
x0 in dom uf0 by A6,A27,XBOOLE_0:def 4;
then
A31: x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C)) by A3,FUNCT_1:11;
A32: uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A6,A28,FUNCT_1:12
.= (Re f).c0 by A31,FUNCT_1:12;
A33: x0 in dom (uf0(#)(r(#)(x`|Z))) by A26,A25,RFUNCT_1:13;then
x0 in dom (uf0) /\ dom (r(#)(x`|Z)) by VALUED_1:def 4;
then
A34: x0 in dom (r(#)(x`|Z)) by XBOOLE_0:def 4;
(u0(#)(x`|Z)).x0 = (u0.x0)*((x`|Z).x0) by A26,VALUED_1:def 4
.= (r*(Re f).c0)*((x`|Z).x0) by A30,VALUED_1:6
.= uf0.x0*(r*((x`|Z).x0)) by A32
.= uf0.x0*(r(#)(x`|Z)).x0 by A34,VALUED_1:def 5
.= (uf0(#)(r(#)(x`|Z))).x0 by A33,VALUED_1:def 4
.= (r(#)(uf0(#)(x`|Z))).x0 by RFUNCT_1:13;
hence thesis;
end;
hence thesis by A6,A23,A24,FUNCT_1:2;
end;
A35: v0(#)(x`|Z) = r(#)(vf0(#)(x`|Z))
proof
A36: dom (r(#)(vf0(#)(x`|Z))) = dom (vf0(#)(r(#)(x`|Z))) by RFUNCT_1:13
.= dom(vf0) /\ dom (r(#)(x`|Z)) by VALUED_1:def 4
.= dom vf0 /\ dom (x`|Z) by VALUED_1:def 5;
A37: dom (v0(#)(x`|Z)) = dom v0 /\ dom (x`|Z) by VALUED_1:def 4;
A38: dom (v0(#)(x`|Z)) = dom (r(#)(vf0(#)(x`|Z))) by A14,A36,VALUED_1:def 4;
for x0 be object st x0 in dom (v0(#)(x`|Z))
holds (v0(#)(x`|Z)).x0 = (r(#)(vf0(#)(x`|Z))).x0
proof
let x0 be object such that
A39: x0 in dom (v0(#)(x`|Z));
A40: x0 in dom v0 /\ dom (x`|Z) by A39,VALUED_1:def 4;then
A41: x0 in dom v0 & x0 in dom (x`|Z) by XBOOLE_0:def 4;
then A42: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (r(#)f))*(R2-to-C))
by A5,FUNCT_1:11;
set R2 = <:x,y:>.x0;
set c0 = (R2-to-C).R2;
A43: v0.x0 = ((Im (r(#)f))*(R2-to-C)).R2 by A5,A41,FUNCT_1:12
.= (Im (r(#)f)).c0 by A42,FUNCT_1:12
.= (r(#)Im f).c0 by MESFUN6C:2;
x0 in dom vf0 by A14,A40,XBOOLE_0:def 4;
then
A44: x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C)) by A3,FUNCT_1:11;
A45: vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A14,A41,FUNCT_1:12
.= (Im f).c0 by A44,FUNCT_1:12;
A46: x0 in dom (vf0(#)(r(#)(x`|Z))) by A38,A39,RFUNCT_1:13;then
x0 in dom (vf0) /\ dom (r(#)(x`|Z)) by VALUED_1:def 4; then
A47: x0 in dom (r(#)(x`|Z)) by XBOOLE_0:def 4;
(v0(#)(x`|Z)).x0 = (v0.x0)*((x`|Z).x0) by A39,VALUED_1:def 4
.= (r*(Im f).c0)*((x`|Z).x0) by A43,VALUED_1:6
.= vf0.x0*(r*((x`|Z).x0)) by A45
.= vf0.x0*(r(#)(x`|Z)).x0 by A47,VALUED_1:def 5
.= (vf0(#)(r(#)(x`|Z))).x0 by A46,VALUED_1:def 4
.= (r(#)(vf0(#)(x`|Z))).x0 by RFUNCT_1:13;
hence thesis;
end;
hence thesis by A14,A36,A37,FUNCT_1:2;
end;
A48: u0(#)(y`|Z) = r(#)(uf0(#)(y`|Z))
proof
A49: dom (r(#)(uf0(#)(y`|Z))) = dom (uf0(#)(r(#)(y`|Z))) by RFUNCT_1:13
.= dom(uf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4
.= dom uf0 /\ dom (y`|Z) by VALUED_1:def 5;
A50: dom (u0(#)(y`|Z)) = dom u0 /\ dom (y`|Z) by VALUED_1:def 4;
A51: dom (u0(#)(y`|Z)) = dom (r(#)(uf0(#)(y`|Z))) by A6,A49,VALUED_1:def 4;
for x0 be object st x0 in dom (u0(#)(y`|Z))
holds (u0(#)(y`|Z)).x0 = (r(#)(uf0(#)(y`|Z))).x0
proof
let x0 be object such that
A52: x0 in dom (u0(#)(y`|Z));
A53: x0 in dom u0 /\ dom (y`|Z) by A52,VALUED_1:def 4;then
A54: x0 in dom u0 & x0 in dom (y`|Z) by XBOOLE_0:def 4;
then A55: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Re (r(#)f))*(R2-to-C))
by A5,FUNCT_1:11;
set R2 = <:x,y:>.x0;
set c0 = (R2-to-C).R2;
A56: u0.x0 = ((Re (r(#)f))*(R2-to-C)).R2 by A5,A54,FUNCT_1:12
.= (Re (r(#)f)).c0 by A55,FUNCT_1:12
.= (r(#)Re f).c0 by MESFUN6C:2;
x0 in dom uf0 by A6,A53,XBOOLE_0:def 4;
then
A57: x0 in dom <:x,y:> & R2 in dom ((Re f)*(R2-to-C)) by A3,FUNCT_1:11;
A58: uf0.x0 = ((Re f)*(R2-to-C)).R2 by A3,A6,A54,FUNCT_1:12
.= (Re f).c0 by A57,FUNCT_1:12;
A59: x0 in dom (uf0(#)(r(#)(y`|Z))) by A51,A52,RFUNCT_1:13;then
x0 in dom (uf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4;
then
A60: x0 in dom (r(#)(y`|Z)) by XBOOLE_0:def 4;
(u0(#)(y`|Z)).x0 = (u0.x0)*((y`|Z).x0) by A52,VALUED_1:def 4
.= (r*(Re f).c0)*((y`|Z).x0) by A56,VALUED_1:6
.= uf0.x0*(r*((y`|Z).x0)) by A58
.= uf0.x0*(r(#)(y`|Z)).x0 by A60,VALUED_1:def 5
.= (uf0(#)(r(#)(y`|Z))).x0 by A59,VALUED_1:def 4
.= (r(#)(uf0(#)(y`|Z))).x0 by RFUNCT_1:13;
hence thesis;
end;
hence thesis by A6,A49,A50,FUNCT_1:2;
end;
A61: v0(#)(y`|Z) = r(#)(vf0(#)(y`|Z))
proof
A62: dom (r(#)(vf0(#)(y`|Z))) = dom (vf0(#)(r(#)(y`|Z))) by RFUNCT_1:13
.= dom(vf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4
.= dom vf0 /\ dom (y`|Z) by VALUED_1:def 5;
A63: dom (v0(#)(y`|Z)) = dom v0 /\ dom (y`|Z) by VALUED_1:def 4;
A64: dom (v0(#)(y`|Z)) = dom (r(#)(vf0(#)(y`|Z))) by A14,A62,VALUED_1:def 4;
for x0 be object st x0 in dom (v0(#)(y`|Z))
holds (v0(#)(y`|Z)).x0 = (r(#)(vf0(#)(y`|Z))).x0
proof
let x0 be object such that
A65: x0 in dom (v0(#)(y`|Z));
A66: x0 in dom v0 /\ dom (y`|Z) by A65,VALUED_1:def 4;then
A67: x0 in dom v0 & x0 in dom (y`|Z) by XBOOLE_0:def 4;
then A68: x0 in dom <:x,y:> & <:x,y:>.x0 in dom ((Im (r(#)f))*(R2-to-C))
by A5,FUNCT_1:11;
set R2 = <:x,y:>.x0;
set c0 = (R2-to-C).R2;
A69: v0.x0 = ((Im (r(#)f))*(R2-to-C)).R2 by A5,A67,FUNCT_1:12
.= (Im (r(#)f)).c0 by A68,FUNCT_1:12
.= (r(#)Im f).c0 by MESFUN6C:2;
x0 in dom vf0 by A14,A66,XBOOLE_0:def 4;
then
A70: x0 in dom <:x,y:> & R2 in dom ((Im f)*(R2-to-C)) by A3,FUNCT_1:11;
A71: vf0.x0 = ((Im f)*(R2-to-C)).R2 by A3,A14,A67,FUNCT_1:12
.= (Im f).c0 by A70,FUNCT_1:12;
A72: x0 in dom (vf0(#)(r(#)(y`|Z))) by A64,A65,RFUNCT_1:13;then
x0 in dom (vf0) /\ dom (r(#)(y`|Z)) by VALUED_1:def 4;
then
A73: x0 in dom (r(#)(y`|Z)) by XBOOLE_0:def 4;
(v0(#)(y`|Z)).x0 = (v0.x0)*((y`|Z).x0) by A65,VALUED_1:def 4
.= (r*(Im f).c0)*((y`|Z).x0) by A69,VALUED_1:6
.= vf0.x0*(r*((y`|Z).x0)) by A71
.= vf0.x0*(r(#)(y`|Z)).x0 by A73,VALUED_1:def 5
.= (vf0(#)(r(#)(y`|Z))).x0 by A72,VALUED_1:def 4
.= (r(#)(vf0(#)(y`|Z))).x0 by RFUNCT_1:13;
hence thesis;
end;
hence thesis by A14,A62,A63,FUNCT_1:2;
end;
A74: [.a,b.] c= dom uf0
proof
let x0 be object such that
A75: x0 in [.a,b.];
A76: C.x0 in rng C by A2,A75,FUNCT_1:3;
A77: x0 in dom x & x0 in dom y by A2,A75;
A78: x0 in dom x /\ dom y by A2,A75,XBOOLE_0:def 4;then
A79: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A78,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A80: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A77,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A2,A75,XBOOLE_0:def 4;
then
A81: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A82: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A83: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A75,A2,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A81,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A82,A83,Def1
.= (R2-to-C).R2 by A78,FUNCT_3:48;then
(R2-to-C).R2 in dom f by A1,A76;then
(R2-to-C).R2 in dom (Re f) by COMSEQ_3:def 3;then
R2 in dom ((Re f)* (R2-to-C)) by A80,FUNCT_1:11;
hence thesis by A3,A79,FUNCT_1:11;
end;
A84: [.a,b.] c= dom vf0
proof
let x0 be object such that
A85: x0 in [.a,b.];
A86: C.x0 in rng C by A2,A85,FUNCT_1:3;
A87: x0 in dom x & x0 in dom y by A2,A85;
A88: x0 in dom x /\ dom y by A2,A85,XBOOLE_0:def 4;then
A89: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A88,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A90: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A87,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A2,A85,XBOOLE_0:def 4; then
A91: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A92: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A93: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A85,A2,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A91,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A92,A93,Def1
.= (R2-to-C).R2 by A88,FUNCT_3:48; then
(R2-to-C).R2 in dom f by A1,A86;then
(R2-to-C).R2 in dom (Im f) by COMSEQ_3:def 4;then
R2 in dom ((Im f)* (R2-to-C)) by A90,FUNCT_1:11;
hence thesis by A3,A89,FUNCT_1:11;
end;
A94: [' a,b '] c= dom (uf0(#)(x`|Z) - vf0(#)(y`|Z))
proof
A95: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 3;
A96: dom (uf0(#)(x`|Z) - vf0(#)(y`|Z))
= dom (uf0(#)(x`|Z)) /\ dom (vf0(#)(y`|Z)) by VALUED_1:12
.= (dom uf0 /\ dom (x`|Z)) /\ dom (vf0(#)(y`|Z)) by VALUED_1:def 4
.= (dom uf0 /\ dom (x`|Z)) /\ (dom vf0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom uf0 /\ ((dom (x`|Z)) /\ (dom vf0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom uf0 /\ ((Z) /\ ((dom (y`|Z)) /\ dom vf0)) by A2,FDIFF_1:def 7
.= dom uf0 /\ (Z /\ (Z /\ dom vf0)) by A2,FDIFF_1:def 7
.= dom uf0 /\ ((Z /\ Z) /\ dom vf0) by XBOOLE_1:16
.= (dom uf0 /\ dom vf0) /\ Z by XBOOLE_1:16;
[.a,b.] c= dom uf0 /\ dom vf0 by A74,A84,XBOOLE_1:19;
hence thesis by A2,A95,A96,XBOOLE_1:19;
end;
A97: [' a,b '] c= dom (vf0(#)(x`|Z) + uf0(#)(y`|Z))
proof
A98: [' a,b '] = [.a,b.] by A2,INTEGRA5:def 3;
A99: dom (vf0(#)(x`|Z) + uf0(#)(y`|Z))
= dom (vf0(#)(x`|Z)) /\ dom (uf0(#)(y`|Z)) by VALUED_1:def 1
.= (dom vf0 /\ dom (x`|Z)) /\ dom (uf0(#)(y`|Z)) by VALUED_1:def 4
.= (dom vf0 /\ dom (x`|Z)) /\ (dom uf0 /\ dom (y`|Z)) by VALUED_1:def 4
.= dom vf0 /\ ((dom (x`|Z)) /\ (dom uf0 /\ dom (y`|Z))) by XBOOLE_1:16
.= dom vf0 /\ ((Z) /\ ((dom (y`|Z)) /\ dom uf0)) by A2,FDIFF_1:def 7
.= dom vf0 /\ (Z /\ (Z /\ dom uf0)) by A2,FDIFF_1:def 7
.= dom vf0 /\ ((Z /\ Z) /\ dom uf0) by XBOOLE_1:16
.= (dom vf0 /\ dom uf0) /\ Z by XBOOLE_1:16;
[.a,b.] c= dom vf0 /\ dom uf0 by A74,A84,XBOOLE_1:19;
hence thesis by A2,A98,A99,XBOOLE_1:19;
end;
reconsider a,b as Real;
A100: (uf0(#)(x`|Z) - vf0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2;
A101: (vf0(#)(x`|Z) + uf0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A2;
A102: (uf0(#)(x`|Z) - vf0(#)(y`|Z))|[' a,b '] is bounded by A1,A2;
A103: (vf0(#)(x`|Z) + uf0(#)(y`|Z))|[' a,b '] is bounded by A1,A2;
integral(r(#)f,C) = integral( r(#)(uf0(#)(x`|Z)) - r(#)(vf0(#)(y`|Z)),a,b )
+ integral( r(#)(vf0(#)(x`|Z)) + r(#)(uf0(#)(y`|Z)),a,b )*<i>
by A35,A61,A48,A22,A5,A1,A2,A4,Def4
.= integral(r(#)(uf0(#)(x`|Z) - vf0(#)(y`|Z)),a,b )
+ integral(r(#)(vf0(#)(x`|Z)) + r(#)(uf0(#)(y`|Z)),a,b )*<i> by RFUNCT_1:18
.= integral(r(#)(uf0(#)(x`|Z) - vf0(#)(y`|Z)),a,b )
+ integral(r(#)(vf0(#)(x`|Z) + uf0(#)(y`|Z)),a,b )*<i> by RFUNCT_1:16
.= r*integral(uf0(#)(x`|Z) - vf0(#)(y`|Z),a,b )
+ integral(r(#)(vf0(#)(x`|Z) + uf0(#)(y`|Z)),a,b )*<i>
by A2,A94,A100,A102,INTEGRA6:10
.= r*integral(uf0(#)(x`|Z) - vf0(#)(y`|Z),a,b )
+ r*integral(vf0(#)(x`|Z) + uf0(#)(y`|Z),a,b )*<i>
by A2,A97,A101,A103,INTEGRA6:10
.= r*(integral(uf0(#)(x`|Z) - vf0(#)(y`|Z),a,b )
+ integral(vf0(#)(x`|Z) + uf0(#)(y`|Z),a,b )*<i>)
.= r*integral(f,C) by A1,A2,A3,Def4;
hence thesis;
end;
begin :: Complex Integral of Complex Curve's Connection
theorem
for f be PartFunc of COMPLEX,COMPLEX, C,C1,C2 be C1-curve, a,b,d be Real
st rng C c= dom f & f is_integrable_on C & f is_bounded_on C &
a <= b & dom C = [.a,b.] & d in [.a,b.] &
dom C1 = [.a,d.] & dom C2 = [.d,b.] &
(for t st t in dom C1 holds C.t = C1.t) &
(for t st t in dom C2 holds C.t = C2.t) holds
integral(f,C) = integral(f,C1) + integral(f,C2)
proof
let f be PartFunc of COMPLEX,COMPLEX,
C,C1,C2 be C1-curve,
a,b,d be Real such that
A1: rng C c= dom f & f is_integrable_on C & f is_bounded_on C &
a <= b & dom C = [.a,b.] & d in [.a,b.] &
dom C1 = [.a,d.] & dom C2 =[.d,b.] &
(for t st t in dom C1 holds C.t = C1.t) &
(for t st t in dom C2 holds C.t = C2.t);
A2: a <= d & d <= b by A1,XXREAL_1:1;
consider a0,b0 be Real, x,y be PartFunc of REAL,REAL,
Z be Subset of REAL such that
A3: a0 <= b0 & [.a0,b0.]=dom C & [.a0,b0.] c= dom x & [.a0,b0.] c= dom y &
Z is open & [.a0,b0.] c= Z & x is_differentiable_on Z &
y is_differentiable_on Z & x`|Z is continuous & y`|Z is continuous &
C = (x+<i>(#)y) | [.a0,b0.] by Def3;
A4: a0 = a & b0 = b
proof
thus a0 = inf [.a0,b0.] by A3,XXREAL_2:25
.= a by A1,A3,XXREAL_2:25;
thus b0 = sup [.a0,b0.] by A3,XXREAL_2:29
.= b by A1,A3,XXREAL_2:29;
end;
consider u0, v0 be PartFunc of REAL,REAL such that
A5: u0=(Re f)* (R2-to-C) *<:x,y:> & v0=(Im f)* (R2-to-C) *<:x,y:> &
integral(f,x,y,a,b,Z)
= integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i> by Def2;
consider a1,b1 be Real,
x1,y1 be PartFunc of REAL,REAL,
Z1 be Subset of REAL such that
A6: a1 <= b1 & [.a1,b1.]=dom C1 & [.a1,b1.] c= dom x1 & [.a1,b1.] c= dom y1
& Z1 is open & [.a1,b1.] c= Z1 & x1 is_differentiable_on Z1 &
y1 is_differentiable_on Z1 & x1`|Z1 is continuous &
y1`|Z1 is continuous &
C1 = (x1+<i>(#)y1) | [.a1,b1.] by Def3;
A7: a1 = a & b1 = d
proof
thus a1 = inf [.a1,b1.] by A6,XXREAL_2:25
.= a by A2,A1,A6,XXREAL_2:25;
thus b1 = sup [.a1,b1.] by A6,XXREAL_2:29
.= d by A2,A1,A6,XXREAL_2:29;
end;
A8: rng C1 c= dom f
proof
A9: [.a,d.] c= [.a,b.] by A2,XXREAL_1:34;
for y0 be object st y0 in rng C1 holds y0 in rng C
proof
let y0 be object such that
A10: y0 in rng C1;
consider x0 be object such that
A11: x0 in dom C1 & y0 = C1.x0 by A10,FUNCT_1:def 3;
C1.x0 = C.x0 by A1,A11;
hence thesis by A1,A9,A11,FUNCT_1:3;
end;then
rng C1 c= rng C;
hence thesis by A1;
end;
consider a2,b2 be Real,
x2,y2 be PartFunc of REAL,REAL,
Z2 be Subset of REAL such that
A12: a2 <= b2 & [.a2,b2.]=dom C2 & [.a2,b2.] c= dom x2 & [.a2,b2.] c= dom y2 &
Z2 is open & [.a2,b2.] c= Z2 &
x2 is_differentiable_on Z2 & y2 is_differentiable_on Z2 &
x2`|Z2 is continuous & y2`|Z2 is continuous &
C2 = (x2+<i>(#)y2) | [.a2,b2.] by Def3;
A13: a2 = d & b2 = b
proof
thus a2 = inf [.a2,b2.] by A12,XXREAL_2:25
.= d by A2,A1,A12,XXREAL_2:25;
thus b2 = sup [.a2,b2.] by A12,XXREAL_2:29
.= b by A2,A1,A12,XXREAL_2:29;
end;
rng C2 c= dom f
proof
A14: [.d,b.] c= [.a,b.] by A2,XXREAL_1:34;
for y0 be object st y0 in rng C2 holds y0 in rng C
proof
let y0 be object such that
A15: y0 in rng C2;
consider x0 be object such that
A16: x0 in dom C2 & y0 = C2.x0 by A15,FUNCT_1:def 3;
C2.x0 = C.x0 by A1,A16;
hence thesis by A1,A14,A16,FUNCT_1:3;
end;then
rng C2 c= rng C;
hence thesis by A1;
end;then
A17: integral(f,C2) = integral(f,x2,y2,d,b,Z2) by A12,A13,Def4;
A18: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
A19: [' a,b '] c= dom u0
proof
for x0 be object st x0 in [.a,b.] holds x0 in dom u0
proof
let x0 be object such that
A20: x0 in [.a,b.];
A21: C.x0 in rng C by A3,A4,A20,FUNCT_1:3;
A22: x0 in dom x & x0 in dom y by A3,A4,A20;
A23: x0 in dom x /\ dom y by A3,A4,A20,XBOOLE_0:def 4;then
A24: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A23,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A25: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A22,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A3,A4,A20,XBOOLE_0:def 4;
then
A26: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A27: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A28: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A20,A3,A4,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A26,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A27,A28,Def1
.= (R2-to-C).R2 by A23,FUNCT_3:48; then
(R2-to-C).R2 in dom f by A1,A21;then
(R2-to-C).R2 in dom (Re f) by COMSEQ_3:def 3;then
R2 in dom ((Re f)* (R2-to-C)) by A25,FUNCT_1:11;
hence thesis by A5,A24,FUNCT_1:11;
end;
hence thesis by A18;
end;
A29: [' a,b '] c= dom v0
proof
for x0 be object st x0 in [.a,b.] holds x0 in dom v0
proof
let x0 be object such that
A30: x0 in [.a,b.];
A31: C.x0 in rng C by A3,A4,A30,FUNCT_1:3;
A32: x0 in dom x & x0 in dom y by A3,A4,A30;
A33: x0 in dom x /\ dom y by A3,A4,A30,XBOOLE_0:def 4;then
A34: x0 in dom <:x,y:> by FUNCT_3:def 7;
set R2 = <:x,y:>.x0;
reconsider xx0 = x.x0, yx0 = y.x0 as Element of REAL by XREAL_0:def 1;
R2 = [xx0,yx0] by A33,FUNCT_3:48;then
R2 in [:REAL,REAL:] by ZFMISC_1:def 2;then
A35: R2 in dom (R2-to-C) by FUNCT_2:def 1;
x0 in dom (<i>(#)y) by A32,VALUED_1:def 5;then
x0 in dom x /\ dom (<i>(#)y) by A3,A4,A30,XBOOLE_0:def 4; then
A36: x0 in dom (x+(<i>(#)y)) by VALUED_1:def 1;
A37: [xx0,yx0] in [:REAL,REAL:] by ZFMISC_1:def 2;
A38: x.x0 = [x.x0,y.x0]`1 & y.x0 = [x.x0,y.x0]`2;
C.x0 = (x+<i>(#)y).x0 by A30,A3,A4,FUNCT_1:49
.= x.x0+(<i>(#)y).x0 by A36,VALUED_1:def 1
.= x.x0+<i>*y.x0 by VALUED_1:6
.= (R2-to-C).([xx0,yx0]) by A37,A38,Def1
.= (R2-to-C).R2 by A33,FUNCT_3:48; then
(R2-to-C).R2 in dom f by A1,A31;then
(R2-to-C).R2 in dom (Im f) by COMSEQ_3:def 4;then
R2 in dom ((Im f)* (R2-to-C)) by A35,FUNCT_1:11;
hence thesis by A5,A34,FUNCT_1:11;
end;
hence thesis by A18;
end;
A39: (u0(#)(x`|Z) - v0(#)(y`|Z)) is_integrable_on [' a,b '] &
(v0(#)(x`|Z) + u0(#)(y`|Z)) is_integrable_on [' a,b '] by A1,A3;
A40: (u0(#)(x`|Z) - v0(#)(y`|Z))|[' a,b '] is bounded &
(v0(#)(x`|Z) + u0(#)(y`|Z))|[' a,b '] is bounded by A1,A3;
A41: [' a,b '] c= dom (u0(#)(x`|Z) - v0(#)(y`|Z))
proof
A42: dom (u0(#)(x`|Z) - v0(#)(y`|Z))
= dom (u0(#)(x`|Z)) /\ dom (v0(#)(y`|Z)) by VALUED_1:12
.= (dom u0 /\ dom(x`|Z)) /\ dom (v0(#)(y`|Z)) by VALUED_1:def 4
.= (dom u0 /\ dom(x`|Z)) /\ (dom v0 /\ dom(y`|Z)) by VALUED_1:def 4
.= (dom u0 /\ Z) /\ (dom v0 /\ dom(y`|Z)) by A3,FDIFF_1:def 7
.= (dom u0 /\ Z) /\ (dom v0 /\ Z) by A3,FDIFF_1:def 7
.= dom u0 /\ (Z /\ (dom v0 /\ Z)) by XBOOLE_1:16
.= dom u0 /\ ((Z /\ Z) /\ dom v0) by XBOOLE_1:16
.= (dom u0 /\ dom v0) /\ Z by XBOOLE_1:16;
A43: [' a,b '] c= dom u0 /\ dom v0 by A19,A29,XBOOLE_1:19;
[' a,b '] c= Z by A1,A3,INTEGRA5:def 3;
hence thesis by A42,A43,XBOOLE_1:19;
end;
A44: [' a,b '] c= dom (v0(#)(x`|Z) + u0(#)(y`|Z))
proof
A45: dom (v0(#)(x`|Z) + u0(#)(y`|Z))
= dom (v0(#)(x`|Z)) /\ dom (u0(#)(y`|Z)) by VALUED_1:def 1
.= (dom v0 /\ dom(x`|Z)) /\ dom (u0(#)(y`|Z)) by VALUED_1:def 4
.= (dom v0 /\ dom(x`|Z)) /\ (dom u0 /\ dom(y`|Z)) by VALUED_1:def 4
.= (dom v0 /\ Z) /\ (dom u0 /\ dom(y`|Z)) by A3,FDIFF_1:def 7
.= (dom v0 /\ Z) /\ (dom u0 /\ Z) by A3,FDIFF_1:def 7
.= dom v0 /\ (Z /\ (dom u0 /\ Z)) by XBOOLE_1:16
.= dom v0 /\ ((Z /\ Z) /\ dom u0) by XBOOLE_1:16
.= (dom v0 /\ dom u0) /\ Z by XBOOLE_1:16;
A46: [' a,b '] c= dom v0 /\ dom u0 by A19,A29,XBOOLE_1:19;
[' a,b '] c= Z by A1,A3,INTEGRA5:def 3;
hence thesis by A45,A46,XBOOLE_1:19;
end;
A47: integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,d )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,d )*<i>
= integral( f,x,y,a,d,Z ) by Def2,A5;
A48: integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,d,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,d,b )*<i>
= integral( f,x,y,d,b,Z ) by Def2,A5;
A49: integral( f,x,y,a,d,Z ) = integral( f,x1,y1,a,d,Z1 )
proof
reconsider Z3 = Z /\ Z1 as Subset of REAL;
reconsider ZZ=Z, ZZ1= Z1 as Subset of R^1 by TOPMETR:17;
ZZ is open & ZZ1 is open by A3,A6,BORSUK_5:39; then
ZZ /\ ZZ1 is open by TOPS_1:11; then
A50: Z3 is open by BORSUK_5:39;
A51: [.a,d.] c= [.a,b.] by A2,XXREAL_1:34;then
A52: [.a,d.] c= dom x & [.a,d.] c= dom y by A3,A4;
A53: x| [.a,d.] = x1| [.a,d.]
proof
A54: dom (x| [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3,A4,A51,XBOOLE_1:1,28
.= (dom x1) /\ [.a,d.] by A6,A7,XBOOLE_1:28
.= dom (x1| [.a,d.]) by RELAT_1:61;
for x0 be object st x0 in dom (x| [.a,d.])
holds (x| [.a,d.]).x0 = (x1| [.a,d.]).x0
proof
let x0 be object such that
A55: x0 in dom (x| [.a,d.]);
A56: dom (x| [.a,d.]) = (dom x) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A51,A3,A4,XBOOLE_1:1,28;
[.a,d.] c= (dom x1) /\ dom y1 by A6,A7,XBOOLE_1:19;then
x0 in (dom x1) /\ dom y1 by A55,A56; then
x0 in (dom x1) /\ dom (<i>(#)y1) by VALUED_1:def 5;then
A57: x0 in dom (x1+<i>(#)y1) by VALUED_1:def 1;
[.a,d.] c= (dom x) /\ dom y by A52,XBOOLE_1:19;then
x0 in (dom x) /\ dom y by A55,A56;then
x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A58: x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A55;
A59: C.t = C1.t by A1,A55,A56;
A60: C.t = (x+<i>(#)y).t by A3,A4,A51,A55,A56,FUNCT_1:49;
A61: C1.t = (x1+<i>(#)y1).t by A6,A7,A55,A56,FUNCT_1:49;
A62: (x1+<i>(#)y1).t = x1.t+(<i>(#)y1).t by A57,VALUED_1:def 1
.= x1.t+<i>*y1.t by VALUED_1:6;
A63: (x+<i>(#)y).t = x.t+(<i>(#)y).t by A58,VALUED_1:def 1
.= x.t+<i>*y.t by VALUED_1:6;
thus (x| [.a,d.]).x0 = x.x0 by A55,FUNCT_1:47
.= x1.x0 by A59,A60,A61,A62,A63,COMPLEX1:77
.= (x1| [.a,d.]).x0 by A56,A55,FUNCT_1:49;
end;
hence thesis by A54,FUNCT_1:2;
end;
A64: y| [.a,d.] = y1| [.a,d.]
proof
A65: dom (y| [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3,A4,A51,XBOOLE_1:1,28
.= (dom y1) /\ [.a,d.] by A6,A7,XBOOLE_1:28
.= dom (y1| [.a,d.]) by RELAT_1:61;
for x0 be object st x0 in dom (y| [.a,d.])
holds (y| [.a,d.]).x0 = (y1| [.a,d.]).x0
proof
let x0 be object such that
A66: x0 in dom (y| [.a,d.]);
A67: dom (y| [.a,d.]) = (dom y) /\ [.a,d.] by RELAT_1:61
.= [.a,d.] by A3,A4,A51,XBOOLE_1:1,28;
[.a,d.] c= (dom x1) /\ dom y1 by A6,A7,XBOOLE_1:19;then
x0 in (dom x1) /\ dom y1 by A66,A67;then
x0 in (dom x1) /\ dom (<i>(#)y1) by VALUED_1:def 5;then
A68: x0 in dom (x1+<i>(#)y1) by VALUED_1:def 1;
[.a,d.] c= (dom x) /\ dom y by A52,XBOOLE_1:19;then
x0 in (dom x) /\ dom y by A66,A67;then
x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A69: x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A66;
A70: C.t = C1.t by A1,A66,A67;
A71: C.t = (x+<i>(#)y).t by A3,A4,A51,A66,A67,FUNCT_1:49;
A72: C1.t = (x1+<i>(#)y1).t by A6,A7,A66,A67,FUNCT_1:49;
A73: (x1+<i>(#)y1).t = x1.t+(<i>(#)y1).t by A68,VALUED_1:def 1
.= x1.t+<i>*y1.t by VALUED_1:6;
A74: (x+<i>(#)y).t = x.t+(<i>(#)y).t by A69,VALUED_1:def 1
.= x.t+<i>*y.t by VALUED_1:6;
thus (y| [.a,d.]).x0 = y.x0 by A66,FUNCT_1:47
.= y1.x0 by A70,A71,A72,A73,A74,COMPLEX1:77
.= (y1| [.a,d.]).x0 by A67,A66,FUNCT_1:49;
end;
hence thesis by A65,FUNCT_1:2;
end;
A75: [.a,d.] c= Z by A3,A4,A51;then
A76: [.a,d.] c= Z3 by A6,A7,XBOOLE_1:19;
A77: rng ((x+<i>(#)y) | [.a,d.]) c= dom f
proof
let y0 be object such that
A78: y0 in rng ((x+<i>(#)y) | [.a,d.]);
consider x0 be object such that
A79: x0 in dom ((x+<i>(#)y) | [.a,d.])
& y0 = ((x+<i>(#)y) | [.a,d.]).x0 by A78,FUNCT_1:def 3;
A80: x0 in (dom (x+<i>(#)y)) /\ [.a,d.] by A79,RELAT_1:61;
(dom (x+<i>(#)y)) /\ [.a,d.] c= (dom (x+<i>(#)y)) /\ [.a,b.]
by A2,XBOOLE_1:26,XXREAL_1:34;then
x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by A80;then
A81: x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:61; then
A82: ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
by FUNCT_1:3;
((x+<i>(#)y) | [.a,d.]).x0 = (x+<i>(#)y).x0 by A79,FUNCT_1:47
.= ((x+<i>(#)y) | [.a,b.]).x0 by A81,FUNCT_1:47;
hence thesis by A1,A3,A79,A82;
end;
A83: rng ((x1+<i>(#)y1) | [.a,d.]) c= dom f
proof
let y0 be object such that
A84: y0 in rng ((x1+<i>(#)y1) | [.a,d.]);
consider x0 be object such that
A85: x0 in dom ((x1+<i>(#)y1) | [.a,d.])
& y0 = ((x1+<i>(#)y1) | [.a,d.]).x0 by A84,FUNCT_1:def 3;
x0 in (dom (x1+<i>(#)y1)) /\ [.a,d.] by A85,RELAT_1:61;
then
A86: x0 in [.a,d.] by XBOOLE_0:def 4;then
x0 in [.a,b.] by A51;
then x0 in (dom x) /\ (dom y) by A3,A4,XBOOLE_0:def 4;then
x0 in ((dom x) /\ (dom y)) /\ [.a,b.] by A51,A86,XBOOLE_0:def 4;
then
x0 in ((dom x) /\ dom (<i>(#)y)) /\ [.a,b.] by VALUED_1:def 5;
then
x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by VALUED_1:def 1;then
x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:61; then
A87: ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
by FUNCT_1:3;
reconsider t = x0 as Element of REAL by A85;
A88: C.t = (x+<i>(#)y).t by A3,A4,A51,A86,FUNCT_1:49;
A89: C1.t = (x1+<i>(#)y1).t by A6,A7,A86,FUNCT_1:49;
((x1+<i>(#)y1) | [.a,d.]).x0 = (x1+<i>(#)y1).x0 by A85,FUNCT_1:47
.= (x+<i>(#)y).x0 by A1,A86,A88,A89
.= ((x+<i>(#)y) | [.a,b.]).x0 by A51,A86,FUNCT_1:49;
hence thesis by A1,A3,A85,A87;
end;
A90: x is_differentiable_on Z3 &
y is_differentiable_on Z3 by A3,A50,FDIFF_1:26,XBOOLE_1:17;
A91: x1 is_differentiable_on Z3 &
y1 is_differentiable_on Z3 by A6,A50,FDIFF_1:26,XBOOLE_1:17;
A92: [.a,d.] c= dom x & [.a,d.] c= dom y by A3,A4,A51;
hence integral(f,x,y,a,d,Z)
= integral(f,x,y,a,d,Z3) by A3,A6,A7,A50,A77,A76,Lm1,XBOOLE_1:17
.= integral(f,x1,y1,a,d,Z3)
by A6,A7,A50,A53,A64,A75,A77,A83,A90,A91,A92,Lm2,XBOOLE_1:19
.= integral(f,x1,y1,a,d,Z1) by A6,A7,A50,A76,A83,Lm1,XBOOLE_1:17;
end;
A93: integral( f,x,y,d,b,Z ) = integral( f,x2,y2,d,b,Z2 )
proof
reconsider Z3 = Z /\ Z2 as Subset of REAL;
reconsider ZZ=Z, ZZ1= Z2 as Subset of R^1 by TOPMETR:17;
ZZ is open & ZZ1 is open by A3,A12,BORSUK_5:39; then
ZZ /\ ZZ1 is open by TOPS_1:11; then
A94: Z3 is open by BORSUK_5:39;
A95: [.d,b.] c= [.a,b.] by A2,XXREAL_1:34;then
A96: [.d,b.] c= dom x & [.d,b.] c= dom y by A3,A4;
A97: x| [.d,b.] = x2| [.d,b.]
proof
A98: dom (x| [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3,A4,A95,XBOOLE_1:1,28
.= (dom x2) /\ [.d,b.] by A12,A13,XBOOLE_1:28
.= dom (x2| [.d,b.]) by RELAT_1:61;
for x0 be object st x0 in dom (x| [.d,b.])
holds (x| [.d,b.]).x0 = (x2| [.d,b.]).x0
proof
let x0 be object such that
A99: x0 in dom (x| [.d,b.]);
A100: dom (x| [.d,b.]) = (dom x) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3,A4,A95,XBOOLE_1:1,28;
[.d,b.] c= (dom x2) /\ dom y2 by A12,A13,XBOOLE_1:19;then
x0 in (dom x2) /\ dom y2 by A99,A100; then
x0 in (dom x2) /\ dom (<i>(#)y2) by VALUED_1:def 5;then
A101: x0 in dom (x2+<i>(#)y2) by VALUED_1:def 1;
[.d,b.] c= (dom x) /\ dom y by A96,XBOOLE_1:19;then
x0 in (dom x) /\ dom y by A99,A100; then
x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A102: x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A99;
A103: C.t = C2.t by A1,A99,A100;
A104: C.t = (x+<i>(#)y).t by A3,A4,A95,A99,A100,FUNCT_1:49;
A105: C2.t = (x2+<i>(#)y2).t by A12,A13,A99,A100,FUNCT_1:49;
A106: (x2+<i>(#)y2).t = x2.t+(<i>(#)y2).t by A101,VALUED_1:def 1
.= x2.t+<i>*y2.t by VALUED_1:6;
A107: (x+<i>(#)y).t = x.t+(<i>(#)y).t by A102,VALUED_1:def 1
.= x.t+<i>*y.t by VALUED_1:6;
thus (x| [.d,b.]).x0 = x.x0 by A99,FUNCT_1:47
.= x2.x0 by A103,A104,A105,A106,A107,COMPLEX1:77
.= (x2| [.d,b.]).x0 by A99,A100,FUNCT_1:49;
end;
hence thesis by A98,FUNCT_1:2;
end;
A108: y| [.d,b.] = y2| [.d,b.]
proof
A109: dom (y| [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3,A4,A95,XBOOLE_1:1,28
.= (dom y2) /\ [.d,b.] by A12,A13,XBOOLE_1:28
.= dom (y2| [.d,b.]) by RELAT_1:61;
for x0 be object st x0 in dom (y| [.d,b.])
holds (y| [.d,b.]).x0 = (y2| [.d,b.]).x0
proof
let x0 be object such that
A110: x0 in dom (y| [.d,b.]);
A111: dom (y| [.d,b.]) = (dom y) /\ [.d,b.] by RELAT_1:61
.= [.d,b.] by A3,A4,A95,XBOOLE_1:1,28;
[.d,b.] c= (dom x2) /\ dom y2 by A12,A13,XBOOLE_1:19;then
x0 in (dom x2) /\ dom y2 by A110,A111;then
x0 in (dom x2) /\ dom (<i>(#)y2) by VALUED_1:def 5;then
A112: x0 in dom (x2+<i>(#)y2) by VALUED_1:def 1;
[.d,b.] c= (dom x) /\ dom y by A96,XBOOLE_1:19;then
x0 in (dom x) /\ dom y by A110,A111;then
x0 in (dom x) /\ dom (<i>(#)y) by VALUED_1:def 5;then
A113: x0 in dom (x+<i>(#)y) by VALUED_1:def 1;
reconsider t = x0 as Element of REAL by A110;
A114: C.t = C2.t by A1,A110,A111;
A115: C.t = (x+<i>(#)y).t by A3,A4,A95,A110,A111,FUNCT_1:49;
A116: C2.t = (x2+<i>(#)y2).t by A12,A13,A110,A111,FUNCT_1:49;
A117: (x2+<i>(#)y2).t = x2.t+(<i>(#)y2).t by A112,VALUED_1:def 1
.= x2.t+<i>*y2.t by VALUED_1:6;
A118: (x+<i>(#)y).t = x.t+(<i>(#)y).t by A113,VALUED_1:def 1
.= x.t+<i>*y.t by VALUED_1:6;
thus (y| [.d,b.]).x0 = y.x0 by A110,FUNCT_1:47
.= y2.x0 by A114,A115,A116,A117,A118,COMPLEX1:77
.= (y2| [.d,b.]).x0 by A111,A110,FUNCT_1:49;
end;
hence thesis by A109,FUNCT_1:2;
end;
A119: [.d,b.] c= Z by A3,A4,A95;then
A120: [.d,b.] c= Z3 by A12,A13,XBOOLE_1:19;
A121: rng ((x+<i>(#)y) | [.d,b.]) c= dom f
proof
let y0 be object such that
A122: y0 in rng ((x+<i>(#)y) | [.d,b.]);
consider x0 be object such that
A123: x0 in dom ((x+<i>(#)y) | [.d,b.]) &
y0 = ((x+<i>(#)y) | [.d,b.]).x0 by A122,FUNCT_1:def 3;
A124: x0 in (dom (x+<i>(#)y)) /\ [.d,b.] by A123,RELAT_1:61;
(dom (x+<i>(#)y)) /\ [.d,b.] c= (dom (x+<i>(#)y)) /\ [.a,b.]
by A2,XBOOLE_1:26,XXREAL_1:34;then
x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by A124;then
A125: x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:61;then
A126: ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
by FUNCT_1:3;
((x+<i>(#)y) | [.d,b.]).x0 = (x+<i>(#)y).x0 by A123,FUNCT_1:47
.= ((x+<i>(#)y) | [.a,b.]).x0 by A125,FUNCT_1:47;
hence thesis by A1,A3,A123,A126;
end;
A127: rng ((x2+<i>(#)y2) | [.d,b.]) c= dom f
proof
let y0 be object such that
A128: y0 in rng ((x2+<i>(#)y2) | [.d,b.]);
consider x0 be object such that
A129: x0 in dom ((x2+<i>(#)y2) | [.d,b.]) &
y0 = ((x2+<i>(#)y2) | [.d,b.]).x0 by A128,FUNCT_1:def 3;
x0 in (dom (x2+<i>(#)y2)) /\ [.d,b.] by A129,RELAT_1:61;
then
A130: x0 in [.d,b.] by XBOOLE_0:def 4;then
x0 in [.a,b.] by A95;
then x0 in (dom x) /\ (dom y) by A3,A4,XBOOLE_0:def 4;then
x0 in ((dom x) /\ (dom y)) /\ [.a,b.] by A95,A130,XBOOLE_0:def 4;
then
x0 in ((dom x) /\ dom (<i>(#)y)) /\ [.a,b.] by VALUED_1:def 5;
then
x0 in (dom (x+<i>(#)y)) /\ [.a,b.] by VALUED_1:def 1;then
x0 in dom ((x+<i>(#)y) | [.a,b.]) by RELAT_1:61;then
A131: ((x+<i>(#)y) | [.a,b.]).x0 in rng ((x+<i>(#)y) | [.a,b.])
by FUNCT_1:3;
reconsider t = x0 as Element of REAL by A129;
A132: C.t = (x+<i>(#)y).t by A3,A4,A95,A130,FUNCT_1:49;
A133: C2.t = (x2+<i>(#)y2).t by A12,A13,A130,FUNCT_1:49;
((x2+<i>(#)y2) | [.d,b.]).x0 = (x2+<i>(#)y2).x0 by A129,FUNCT_1:47
.= (x+<i>(#)y).x0 by A1,A130,A132,A133
.= ((x+<i>(#)y) | [.a,b.]).x0 by A95,A130,FUNCT_1:49;
hence thesis by A1,A3,A129,A131;
end;
A134: x is_differentiable_on Z3 &
y is_differentiable_on Z3 by A3,A94,FDIFF_1:26,XBOOLE_1:17;
A135: x2 is_differentiable_on Z3 &
y2 is_differentiable_on Z3 by A12,A94,FDIFF_1:26,XBOOLE_1:17;
A136: [.d,b.] c= dom x & [.d,b.] c= dom y by A3,A4,A95;
hence integral(f,x,y,d,b,Z) = integral(f,x,y,d,b,Z3)
by A3,A12,A13,A94,A120,A121,Lm1,XBOOLE_1:17
.= integral(f,x2,y2,d,b,Z3)
by Lm2,A12,A13,A94,A97,A108,A119,A121,A127,A134,A135,A136,XBOOLE_1:19
.= integral(f,x2,y2,d,b,Z2) by A12,A13,A94,A120,A127,Lm1,XBOOLE_1:17;
end;
thus integral(f,C) = integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i> by A1,A3,A5,Def4
.= integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,d )
+ integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,d,b )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,b )*<i>
by A1,A18,A39,A40,A41,INTEGRA6:17
.= integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,a,d )
+ integral( u0(#)(x`|Z) - v0(#)(y`|Z) ,d,b )
+(integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,a,d )
+ integral( v0(#)(x`|Z) + u0(#)(y`|Z) ,d,b ))*<i>
by A1,A18,A39,A40,A44,INTEGRA6:17
.= integral( f,x1,y1,a,d,Z1 ) + integral( f,x,y,d,b,Z ) by A49,A48,A47
.= integral(f,C1) + integral(f,C2) by A6,A7,A8,A17,Def4,A93;
end;