let a, b be Real; for x, y being PartFunc of REAL,REAL
for Z1, Z2 being Subset of REAL
for f being 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)
let x, y be PartFunc of REAL,REAL; for Z1, Z2 being Subset of REAL
for f being 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)
let Z1, Z2 be Subset of REAL; for f being 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)
let f be PartFunc of COMPLEX,COMPLEX; ( 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 implies integral (f,x,y,a,b,Z1) = integral (f,x,y,a,b,Z2) )
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 )
; integral (f,x,y,a,b,Z1) = integral (f,x,y,a,b,Z2)
then A2:
( x is_differentiable_on Z1 & y is_differentiable_on Z1 )
by FDIFF_1:26;
consider u01, v01 being 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 being 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, XBOOLE_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 be
object ;
( x0 in dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) implies (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0 )
assume A10:
x0 in dom (((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB)
;
(((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0
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 =
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
(((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB) . x0 = (((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB) . x0
by A2, A13, A14, FDIFF_1:def 7;
verum
end;
hence
((u01 (#) (x `| Z1)) - (v01 (#) (y `| Z1))) | AB = ((u02 (#) (x `| Z2)) - (v02 (#) (y `| Z2))) | AB
by A8, A9, FUNCT_1:def 11;
verum
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, XBOOLE_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 be
object ;
( x0 in dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) implies (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0 )
assume A24:
x0 in dom (((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB)
;
(((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0
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 =
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
(((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB) . x0 = (((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB) . x0
by A1, A3, A4, A29, A32, FDIFF_1:def 7;
verum
end;
hence
((v01 (#) (x `| Z1)) + (u01 (#) (y `| Z1))) | AB = ((v02 (#) (x `| Z2)) + (u02 (#) (y `| Z2))) | AB
by A22, A23, FUNCT_1:def 11;
verum
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
integral (f,x,y,a,b,Z1) = integral (f,x,y,a,b,Z2)
by A3, A4, A18; verum