let f, g be PartFunc of COMPLEX,COMPLEX; for C being 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))
let C be C1-curve; ( 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 implies integral ((f + g),C) = (integral (f,C)) + (integral (g,C)) )
assume 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 )
; integral ((f + g),C) = (integral (f,C)) + (integral (g,C))
consider a, b being Real, x, y being PartFunc of REAL,REAL, Z being 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 = a, b = b as Real ;
consider uf0, vf0 being 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 being 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 being 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 being
object st
x0 in dom u0 holds
x0 in (dom uf0) /\ (dom ug0)
proof
let x0 be
object ;
( x0 in dom u0 implies x0 in (dom uf0) /\ (dom ug0) )
assume A14:
x0 in dom u0
;
x0 in (dom uf0) /\ (dom ug0)
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) )
by A15, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g))
by MESFUN6C:5;
then
R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g))
by VALUED_1:def 1;
then
(
R2-to-C . (<:x,y:> . x0) in dom (Re f) &
R2-to-C . (<:x,y:> . x0) in dom (Re g) )
by XBOOLE_0:def 4;
then
(
<:x,y:> . x0 in dom ((Re f) * R2-to-C) &
<:x,y:> . x0 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
x0 in (dom uf0) /\ (dom ug0)
by XBOOLE_0:def 4;
verum
end;
for
x0 being
object st
x0 in (dom uf0) /\ (dom ug0) holds
x0 in dom u0
proof
let x0 be
object ;
( x0 in (dom uf0) /\ (dom ug0) implies x0 in dom u0 )
assume A17:
x0 in (dom uf0) /\ (dom ug0)
;
x0 in dom u0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re f) )
by A19, FUNCT_1:11;
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re g) )
by A20, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g))
by A21, XBOOLE_0:def 4;
then
R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g))
by VALUED_1:def 1;
then
R2-to-C . (<:x,y:> . x0) in dom (Re (f + g))
by MESFUN6C:5;
then
<:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C)
by A21, FUNCT_1:11;
hence
x0 in dom u0
by A8, A19, FUNCT_1:11;
verum
end;
hence
dom u0 = (dom uf0) /\ (dom ug0)
by A13, TARSKI:2;
verum
end;
for
x0 being
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 ;
( x0 in dom (u0 (#) (x `| Z)) implies (u0 (#) (x `| Z)) . x0 = ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0 )
assume A22:
x0 in dom (u0 (#) (x `| Z))
;
(u0 (#) (x `| Z)) . x0 = ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) )
by A24, FUNCT_1:11;
set c0 =
R2-to-C . (<:x,y:> . x0);
A26:
u0 . x0 =
((Re (f + g)) * R2-to-C) . (<:x,y:> . x0)
by A8, A23, FUNCT_1:12
.=
(Re (f + g)) . (R2-to-C . (<:x,y:> . x0))
by A24, FUNCT_1:12
.=
((Re f) + (Re g)) . (R2-to-C . (<:x,y:> . x0))
by MESFUN6C:5
;
A27:
R2-to-C . (<:x,y:> . x0) 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:> &
<:x,y:> . x0 in dom ((Re f) * R2-to-C) )
by A3, FUNCT_1:11;
A30:
uf0 . x0 =
((Re f) * R2-to-C) . (<:x,y:> . x0)
by A3, A28, FUNCT_1:12
.=
(Re f) . (R2-to-C . (<:x,y:> . x0))
by A29, FUNCT_1:12
;
A31:
(
x0 in dom <:x,y:> &
<:x,y:> . x0 in dom ((Re g) * R2-to-C) )
by A4, A28, FUNCT_1:11;
A32:
ug0 . x0 =
((Re g) * R2-to-C) . (<:x,y:> . x0)
by A4, A28, FUNCT_1:12
.=
(Re g) . (R2-to-C . (<:x,y:> . x0))
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) . (R2-to-C . (<:x,y:> . x0))) * ((x `| Z) . x0)
by A30, VALUED_1:def 4;
A35:
(ug0 (#) (x `| Z)) . x0 = ((Re g) . (R2-to-C . (<:x,y:> . x0))) * ((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) . (R2-to-C . (<:x,y:> . x0))) + ((Re g) . (R2-to-C . (<:x,y:> . x0)))) * ((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
(u0 (#) (x `| Z)) . x0 = ((uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))) . x0
;
verum
end;
hence
u0 (#) (x `| Z) = (uf0 (#) (x `| Z)) + (ug0 (#) (x `| Z))
by A10, A11, A12, FUNCT_1:2;
verum
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 being
object st
x0 in dom v0 holds
x0 in (dom vf0) /\ (dom vg0)
proof
let x0 be
object ;
( x0 in dom v0 implies x0 in (dom vf0) /\ (dom vg0) )
assume A41:
x0 in dom v0
;
x0 in (dom vf0) /\ (dom vg0)
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) )
by A42, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g))
by MESFUN6C:5;
then
R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g))
by VALUED_1:def 1;
then
(
R2-to-C . (<:x,y:> . x0) in dom (Im f) &
R2-to-C . (<:x,y:> . x0) in dom (Im g) )
by XBOOLE_0:def 4;
then
(
<:x,y:> . x0 in dom ((Im f) * R2-to-C) &
<:x,y:> . x0 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
x0 in (dom vf0) /\ (dom vg0)
by XBOOLE_0:def 4;
verum
end;
for
x0 being
object st
x0 in (dom vf0) /\ (dom vg0) holds
x0 in dom v0
proof
let x0 be
object ;
( x0 in (dom vf0) /\ (dom vg0) implies x0 in dom v0 )
assume A44:
x0 in (dom vf0) /\ (dom vg0)
;
x0 in dom v0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im f) )
by A46, FUNCT_1:11;
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im g) )
by A47, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g))
by A48, XBOOLE_0:def 4;
then
R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g))
by VALUED_1:def 1;
then
R2-to-C . (<:x,y:> . x0) in dom (Im (f + g))
by MESFUN6C:5;
then
<:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C)
by A48, FUNCT_1:11;
hence
x0 in dom v0
by A8, A46, FUNCT_1:11;
verum
end;
hence
dom v0 = (dom vf0) /\ (dom vg0)
by A40, TARSKI:2;
verum
end;
for
x0 being
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 ;
( x0 in dom (v0 (#) (x `| Z)) implies (v0 (#) (x `| Z)) . x0 = ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0 )
assume A49:
x0 in dom (v0 (#) (x `| Z))
;
(v0 (#) (x `| Z)) . x0 = ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) )
by A51, FUNCT_1:11;
set c0 =
R2-to-C . (<:x,y:> . x0);
A53:
v0 . x0 =
((Im (f + g)) * R2-to-C) . (<:x,y:> . x0)
by A8, A50, FUNCT_1:12
.=
(Im (f + g)) . (R2-to-C . (<:x,y:> . x0))
by A51, FUNCT_1:12
.=
((Im f) + (Im g)) . (R2-to-C . (<:x,y:> . x0))
by MESFUN6C:5
;
A54:
R2-to-C . (<:x,y:> . x0) 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:> &
<:x,y:> . x0 in dom ((Im f) * R2-to-C) )
by A3, FUNCT_1:11;
A57:
vf0 . x0 =
((Im f) * R2-to-C) . (<:x,y:> . x0)
by A3, A55, FUNCT_1:12
.=
(Im f) . (R2-to-C . (<:x,y:> . x0))
by A56, FUNCT_1:12
;
A58:
(
x0 in dom <:x,y:> &
<:x,y:> . x0 in dom ((Im g) * R2-to-C) )
by A4, A55, FUNCT_1:11;
A59:
vg0 . x0 =
((Im g) * R2-to-C) . (<:x,y:> . x0)
by A4, A55, FUNCT_1:12
.=
(Im g) . (R2-to-C . (<:x,y:> . x0))
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) . (R2-to-C . (<:x,y:> . x0))) * ((x `| Z) . x0)
by A57, VALUED_1:def 4;
A62:
(vg0 (#) (x `| Z)) . x0 = ((Im g) . (R2-to-C . (<:x,y:> . x0))) * ((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) . (R2-to-C . (<:x,y:> . x0))) + ((Im g) . (R2-to-C . (<:x,y:> . x0)))) * ((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
(v0 (#) (x `| Z)) . x0 = ((vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))) . x0
;
verum
end;
hence
v0 (#) (x `| Z) = (vf0 (#) (x `| Z)) + (vg0 (#) (x `| Z))
by A37, A38, A39, FUNCT_1:2;
verum
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 being
object st
x0 in dom u0 holds
x0 in (dom uf0) /\ (dom ug0)
proof
let x0 be
object ;
( x0 in dom u0 implies x0 in (dom uf0) /\ (dom ug0) )
assume A68:
x0 in dom u0
;
x0 in (dom uf0) /\ (dom ug0)
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) )
by A69, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g))
by MESFUN6C:5;
then
R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g))
by VALUED_1:def 1;
then
(
R2-to-C . (<:x,y:> . x0) in dom (Re f) &
R2-to-C . (<:x,y:> . x0) in dom (Re g) )
by XBOOLE_0:def 4;
then
(
<:x,y:> . x0 in dom ((Re f) * R2-to-C) &
<:x,y:> . x0 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
x0 in (dom uf0) /\ (dom ug0)
by XBOOLE_0:def 4;
verum
end;
for
x0 being
object st
x0 in (dom uf0) /\ (dom ug0) holds
x0 in dom u0
proof
let x0 be
object ;
( x0 in (dom uf0) /\ (dom ug0) implies x0 in dom u0 )
assume A71:
x0 in (dom uf0) /\ (dom ug0)
;
x0 in dom u0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re f) )
by A73, FUNCT_1:11;
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re g) )
by A74, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in (dom (Re f)) /\ (dom (Re g))
by A75, XBOOLE_0:def 4;
then
R2-to-C . (<:x,y:> . x0) in dom ((Re f) + (Re g))
by VALUED_1:def 1;
then
R2-to-C . (<:x,y:> . x0) in dom (Re (f + g))
by MESFUN6C:5;
then
<:x,y:> . x0 in dom ((Re (f + g)) * R2-to-C)
by A75, FUNCT_1:11;
hence
x0 in dom u0
by A8, A73, FUNCT_1:11;
verum
end;
hence
dom u0 = (dom uf0) /\ (dom ug0)
by A67, TARSKI:2;
verum
end;
for
x0 being
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 ;
( x0 in dom (u0 (#) (y `| Z)) implies (u0 (#) (y `| Z)) . x0 = ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0 )
assume A76:
x0 in dom (u0 (#) (y `| Z))
;
(u0 (#) (y `| Z)) . x0 = ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Re (f + g)) )
by A78, FUNCT_1:11;
set c0 =
R2-to-C . (<:x,y:> . x0);
A80:
u0 . x0 =
((Re (f + g)) * R2-to-C) . (<:x,y:> . x0)
by A8, A77, FUNCT_1:12
.=
(Re (f + g)) . (R2-to-C . (<:x,y:> . x0))
by A78, FUNCT_1:12
.=
((Re f) + (Re g)) . (R2-to-C . (<:x,y:> . x0))
by MESFUN6C:5
;
A81:
R2-to-C . (<:x,y:> . x0) 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:> &
<:x,y:> . x0 in dom ((Re f) * R2-to-C) )
by A3, FUNCT_1:11;
A84:
uf0 . x0 =
((Re f) * R2-to-C) . (<:x,y:> . x0)
by A3, A82, FUNCT_1:12
.=
(Re f) . (R2-to-C . (<:x,y:> . x0))
by A83, FUNCT_1:12
;
A85:
(
x0 in dom <:x,y:> &
<:x,y:> . x0 in dom ((Re g) * R2-to-C) )
by A4, A82, FUNCT_1:11;
A86:
ug0 . x0 =
((Re g) * R2-to-C) . (<:x,y:> . x0)
by A4, A82, FUNCT_1:12
.=
(Re g) . (R2-to-C . (<:x,y:> . x0))
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) . (R2-to-C . (<:x,y:> . x0))) * ((y `| Z) . x0)
by A84, VALUED_1:def 4;
A89:
(ug0 (#) (y `| Z)) . x0 = ((Re g) . (R2-to-C . (<:x,y:> . x0))) * ((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) . (R2-to-C . (<:x,y:> . x0))) + ((Re g) . (R2-to-C . (<:x,y:> . x0)))) * ((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
(u0 (#) (y `| Z)) . x0 = ((uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))) . x0
;
verum
end;
hence
u0 (#) (y `| Z) = (uf0 (#) (y `| Z)) + (ug0 (#) (y `| Z))
by A64, A65, A66, FUNCT_1:2;
verum
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 being
object st
x0 in dom v0 holds
x0 in (dom vf0) /\ (dom vg0)
proof
let x0 be
object ;
( x0 in dom v0 implies x0 in (dom vf0) /\ (dom vg0) )
assume A95:
x0 in dom v0
;
x0 in (dom vf0) /\ (dom vg0)
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) )
by A96, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g))
by MESFUN6C:5;
then
R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g))
by VALUED_1:def 1;
then
(
R2-to-C . (<:x,y:> . x0) in dom (Im f) &
R2-to-C . (<:x,y:> . x0) in dom (Im g) )
by XBOOLE_0:def 4;
then
(
<:x,y:> . x0 in dom ((Im f) * R2-to-C) &
<:x,y:> . x0 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
x0 in (dom vf0) /\ (dom vg0)
by XBOOLE_0:def 4;
verum
end;
for
x0 being
object st
x0 in (dom vf0) /\ (dom vg0) holds
x0 in dom v0
proof
let x0 be
object ;
( x0 in (dom vf0) /\ (dom vg0) implies x0 in dom v0 )
assume A98:
x0 in (dom vf0) /\ (dom vg0)
;
x0 in dom v0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im f) )
by A100, FUNCT_1:11;
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im g) )
by A101, FUNCT_1:11;
then
R2-to-C . (<:x,y:> . x0) in (dom (Im f)) /\ (dom (Im g))
by A102, XBOOLE_0:def 4;
then
R2-to-C . (<:x,y:> . x0) in dom ((Im f) + (Im g))
by VALUED_1:def 1;
then
R2-to-C . (<:x,y:> . x0) in dom (Im (f + g))
by MESFUN6C:5;
then
<:x,y:> . x0 in dom ((Im (f + g)) * R2-to-C)
by A102, FUNCT_1:11;
hence
x0 in dom v0
by A8, A100, FUNCT_1:11;
verum
end;
hence
dom v0 = (dom vf0) /\ (dom vg0)
by A94, TARSKI:2;
verum
end;
for
x0 being
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 ;
( x0 in dom (v0 (#) (y `| Z)) implies (v0 (#) (y `| Z)) . x0 = ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0 )
assume A103:
x0 in dom (v0 (#) (y `| Z))
;
(v0 (#) (y `| Z)) . x0 = ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0
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:
(
<:x,y:> . x0 in dom R2-to-C &
R2-to-C . (<:x,y:> . x0) in dom (Im (f + g)) )
by A105, FUNCT_1:11;
set c0 =
R2-to-C . (<:x,y:> . x0);
A107:
v0 . x0 =
((Im (f + g)) * R2-to-C) . (<:x,y:> . x0)
by A8, A104, FUNCT_1:12
.=
(Im (f + g)) . (R2-to-C . (<:x,y:> . x0))
by A105, FUNCT_1:12
.=
((Im f) + (Im g)) . (R2-to-C . (<:x,y:> . x0))
by MESFUN6C:5
;
A108:
R2-to-C . (<:x,y:> . x0) 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:> &
<:x,y:> . x0 in dom ((Im f) * R2-to-C) )
by A3, FUNCT_1:11;
A111:
vf0 . x0 =
((Im f) * R2-to-C) . (<:x,y:> . x0)
by A3, A109, FUNCT_1:12
.=
(Im f) . (R2-to-C . (<:x,y:> . x0))
by A110, FUNCT_1:12
;
A112:
(
x0 in dom <:x,y:> &
<:x,y:> . x0 in dom ((Im g) * R2-to-C) )
by A4, A109, FUNCT_1:11;
A113:
vg0 . x0 =
((Im g) * R2-to-C) . (<:x,y:> . x0)
by A4, A109, FUNCT_1:12
.=
(Im g) . (R2-to-C . (<:x,y:> . x0))
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) . (R2-to-C . (<:x,y:> . x0))) * ((y `| Z) . x0)
by A111, VALUED_1:def 4;
A116:
(vg0 (#) (y `| Z)) . x0 = ((Im g) . (R2-to-C . (<:x,y:> . x0))) * ((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) . (R2-to-C . (<:x,y:> . x0))) + ((Im g) . (R2-to-C . (<:x,y:> . x0)))) * ((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
(v0 (#) (y `| Z)) . x0 = ((vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))) . x0
;
verum
end;
hence
v0 (#) (y `| Z) = (vf0 (#) (y `| Z)) + (vg0 (#) (y `| Z))
by A91, A92, A93, FUNCT_1:2;
verum
end;
A117:
[.a,b.] c= dom uf0
proof
let x0 be
object ;
TARSKI:def 3 ( not x0 in [.a,b.] or x0 in dom uf0 )
assume A118:
x0 in [.a,b.]
;
x0 in dom uf0
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;
<:x,y:> . x0 = [xx0,yx0]
by A121, FUNCT_3:48;
then
<:x,y:> . x0 in [:REAL,REAL:]
by ZFMISC_1:def 2;
then A123:
<:x,y:> . x0 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 . (<:x,y:> . x0)
by A121, FUNCT_3:48
;
then
R2-to-C . (<:x,y:> . x0) in dom f
by A1, A119;
then
R2-to-C . (<:x,y:> . x0) in dom (Re f)
by COMSEQ_3:def 3;
then
<:x,y:> . x0 in dom ((Re f) * R2-to-C)
by A123, FUNCT_1:11;
hence
x0 in dom uf0
by A3, A122, FUNCT_1:11;
verum
end;
A127:
[.a,b.] c= dom vf0
proof
let x0 be
object ;
TARSKI:def 3 ( not x0 in [.a,b.] or x0 in dom vf0 )
assume A128:
x0 in [.a,b.]
;
x0 in dom vf0
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;
<:x,y:> . x0 = [xx0,yx0]
by A131, FUNCT_3:48;
then
<:x,y:> . x0 in [:REAL,REAL:]
by ZFMISC_1:def 2;
then A133:
<:x,y:> . x0 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 . (<:x,y:> . x0)
by A131, FUNCT_3:48
;
then
R2-to-C . (<:x,y:> . x0) in dom f
by A1, A129;
then
R2-to-C . (<:x,y:> . x0) in dom (Im f)
by COMSEQ_3:def 4;
then
<:x,y:> . x0 in dom ((Im f) * R2-to-C)
by A133, FUNCT_1:11;
hence
x0 in dom vf0
by A3, A132, FUNCT_1:11;
verum
end;
A137:
[.a,b.] c= dom ug0
proof
let x0 be
object ;
TARSKI:def 3 ( not x0 in [.a,b.] or x0 in dom ug0 )
assume A138:
x0 in [.a,b.]
;
x0 in dom ug0
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;
<:x,y:> . x0 = [xx0,yx0]
by A141, FUNCT_3:48;
then
<:x,y:> . x0 in [:REAL,REAL:]
by ZFMISC_1:def 2;
then A143:
<:x,y:> . x0 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 . (<:x,y:> . x0)
by A141, FUNCT_3:48
;
then
R2-to-C . (<:x,y:> . x0) in dom g
by A1, A139;
then
R2-to-C . (<:x,y:> . x0) in dom (Re g)
by COMSEQ_3:def 3;
then
<:x,y:> . x0 in dom ((Re g) * R2-to-C)
by A143, FUNCT_1:11;
hence
x0 in dom ug0
by A4, A142, FUNCT_1:11;
verum
end;
A147:
[.a,b.] c= dom vg0
proof
let x0 be
object ;
TARSKI:def 3 ( not x0 in [.a,b.] or x0 in dom vg0 )
assume A148:
x0 in [.a,b.]
;
x0 in dom vg0
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;
<:x,y:> . x0 = [xx0,yx0]
by A151, FUNCT_3:48;
then
<:x,y:> . x0 in [:REAL,REAL:]
by ZFMISC_1:def 2;
then A153:
<:x,y:> . x0 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 . (<:x,y:> . x0)
by A151, FUNCT_3:48
;
then
R2-to-C . (<:x,y:> . x0) in dom g
by A1, A149;
then
R2-to-C . (<:x,y:> . x0) in dom (Im g)
by COMSEQ_3:def 4;
then
<:x,y:> . x0 in dom ((Im g) * R2-to-C)
by A153, FUNCT_1:11;
hence
x0 in dom vg0
by A4, A152, FUNCT_1:11;
verum
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
['a,b'] c= dom ((uf0 (#) (x `| Z)) - (vf0 (#) (y `| Z)))
by A2, A158, A159, XBOOLE_1:19;
verum
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
['a,b'] c= dom ((ug0 (#) (x `| Z)) - (vg0 (#) (y `| Z)))
by A2, A161, A162, XBOOLE_1:19;
verum
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
['a,b'] c= dom ((vf0 (#) (x `| Z)) + (uf0 (#) (y `| Z)))
by A2, A164, A165, XBOOLE_1:19;
verum
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
['a,b'] c= dom ((vg0 (#) (x `| Z)) + (ug0 (#) (y `| Z)))
by A2, A167, A168, XBOOLE_1:19;
verum
end;
reconsider a = a, b = 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
integral ((f + g),C) = (integral (f,C)) + (integral (g,C))
; verum